fact: Definition Tensor_Moebius_Q_r (xi:Tensor) y := 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*y+b,c*y+d),(e*y+f,g*y+h)).
imports: Streams Streams_addenda Raxioms