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