fact: Definition Tensor_Moebius_Q_l (xi:Tensor) x := let (a,b) := (fst (fst (fst xi)), snd (fst (fst xi))) in let (c,d) := (fst (snd (fst xi)), snd (snd (fst xi))) in let (e,f) := (fst (fst (snd xi)), snd (fst (snd xi))) in let (g,h) := (fst (snd (snd xi)), snd (snd (snd xi))) in ((a*x+c,b*x+d),(e*x+g,f*x+h)).
imports: Streams Streams_addenda Raxioms