let f, g, h, k be FinSequence of REAL ; :: thesis: ( len f = len h & len g = len k implies sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) )
assume that
A1: len f = len h and
A2: len g = len k ; :: thesis: sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:22;
A5: len (sqr ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th8
.= len (f ^ g) by A1, A2, A3, A4, Th6
.= (len (f + h)) + (len g) by A1, A3, Th6
.= (len (f + h)) + (len (g + k)) by A2, Th6
.= (len (sqr (f + h))) + (len (g + k)) by Th8
.= (len (sqr (f + h))) + (len (sqr (g + k))) by Th8
.= len ((sqr (f + h)) ^ (sqr (g + k))) by FINSEQ_1:22 ;
for i being Nat st 1 <= i & i <= len (sqr ((f ^ g) + (h ^ k))) holds
(sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (sqr ((f ^ g) + (h ^ k))) implies (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i )
assume that
A6: 1 <= i and
A7: i <= len (sqr ((f ^ g) + (h ^ k))) ; :: thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i
i in dom (sqr ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:25;
then A8: i in dom ((f ^ g) + (h ^ k)) by Th8;

per cases ( i in dom f or not i in dom f ) ;

suppose A9: i in dom f ; :: thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i

then A10: i in dom (f + h) by A1, Th6;
then A11: i in dom (sqr (f + h)) by Th8;
A12: i in dom h by A1, A9, FINSEQ_3:29;
thus (sqr ((f ^ g) + (h ^ k))) . i = (((f ^ g) + (h ^ k)) . i) ^2 by VALUED_1:11
.= (((f ^ g) . i) + ((h ^ k) . i)) ^2 by A8, VALUED_1:def 1
.= ((f . i) + ((h ^ k) . i)) ^2 by A9, FINSEQ_1:def 7
.= ((f . i) + (h . i)) ^2 by A12, FINSEQ_1:def 7
.= ((f + h) . i) ^2 by A10, VALUED_1:def 1
.= (sqr (f + h)) . i by VALUED_1:11
.= ((sqr (f + h)) ^ (sqr (g + k))) . i by A11, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: (sqr ((f ^ g) + (h ^ k))) . i = ((sqr (f + h)) ^ (sqr (g + k))) . i

then A13: len f < i by A6, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A14: len (f + h) < i by A1, A13, Th6;
then A15: len (sqr (f + h)) < i by Th8;
i <= len ((f ^ g) + (h ^ k)) by A7, Th8;
then A16: i <= len (f ^ g) by A1, A2, A3, A4, Th6;
then i <= (len (f + h)) + (len g) by A1, A3, Th6;
then i <= (len (f + h)) + (len (g + k)) by A2, Th6;
then i - (len (f + h)) in dom (g + k) by A14, Th4;
then A17: j in dom (g + k) by A1, Th6;
len f = len (f + h) by A1, Th6;
then A18: j = i - (len (sqr (f + h))) by Th8;
thus (sqr ((f ^ g) + (h ^ k))) . i = (((f ^ g) + (h ^ k)) . i) ^2 by VALUED_1:11
.= (((f ^ g) . i) + ((h ^ k) . i)) ^2 by A8, VALUED_1:def 1
.= ((g . j) + ((h ^ k) . i)) ^2 by A13, A16, FINSEQ_1:24
.= ((g . j) + (k . j)) ^2 by A1, A2, A3, A4, A13, A16, FINSEQ_1:24
.= ((g + k) . j) ^2 by A17, VALUED_1:def 1
.= (sqr (g + k)) . j by VALUED_1:11
.= ((sqr (f + h)) ^ (sqr (g + k))) . i by A5, A7, A15, A18, FINSEQ_1:24 ; :: thesis: verum

end;

end;

end;

hence sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k)) by A5, FINSEQ_1:14; :: thesis: verum