let a1, a2, b1, b2 be Complex; :: thesis: for n being Nat
for f, g being b₁ -element complex-valued FinSequence holds (f ^ <*a1,a2*>) + (g ^ <*b1,b2*>) = (f + g) ^ <*(a1 + b1),(a2 + b2)*>
let n be Nat; :: thesis: for f, g being n -element complex-valued FinSequence holds (f ^ <*a1,a2*>) + (g ^ <*b1,b2*>) = (f + g) ^ <*(a1 + b1),(a2 + b2)*>
let f, g be n -element complex-valued FinSequence; :: thesis: (f ^ <*a1,a2*>) + (g ^ <*b1,b2*>) = (f + g) ^ <*(a1 + b1),(a2 + b2)*>
A1: ( f ^ <*a1,a2*> = (f ^ <*a1*>) ^ <*a2*> & g ^ <*b1,b2*> = (g ^ <*b1*>) ^ <*b2*> ) by FINSEQ_1:32;
(f + g) ^ <*(a1 + b1),(a2 + b2)*> = ((f + g) ^ <*(a1 + b1)*>) ^ <*(a2 + b2)*> by FINSEQ_1:32
.= ((f ^ <*a1*>) + (g ^ <*b1*>)) ^ <*(a2 + b2)*> by FINSEQ_9:40
.= ((f ^ <*a1*>) ^ <*a2*>) + ((g ^ <*b1*>) ^ <*b2*>) by FINSEQ_9:40 ;
hence (f ^ <*a1,a2*>) + (g ^ <*b1,b2*>) = (f + g) ^ <*(a1 + b1),(a2 + b2)*> by A1; :: thesis: verum