let f, g be FinSequence of REAL ; :: thesis: sqr (f ^ g) = (sqr f) ^ (sqr g)
A1: len f = len (sqr f) by Th9;
A2: len g = len (sqr g) by Th9;
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
A4: len (sqr (f ^ g)) = len (f ^ g) by Th9;
then A5: len (sqr (f ^ g)) = len ((sqr f) ^ (sqr g)) by A1, A2, A3, FINSEQ_1:35;
for i being Nat st 1 <= i & i <= len (sqr (f ^ g)) holds
(sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (sqr (f ^ g)) implies (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i )
assume A6: ( 1 <= i & i <= len (sqr (f ^ g)) ) ; :: thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i
then A7: i in dom (f ^ g) by A4, FINSEQ_3:27;

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

suppose A8: i in dom f ; :: thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i

then A9: i in dom (sqr f) by Th9;
thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i by RVSUM_1:def 8
.= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:23
.= sqrreal . (f . i) by A8, FINSEQ_1:def 7
.= (f . i) ^2 by RVSUM_1:def 2
.= (sqr f) . i by VALUED_1:11
.= ((sqr f) ^ (sqr g)) . i by A9, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

then A10: ( len f < i & i <= len (f ^ g) ) by A6, Th9, FINSEQ_3:27;
then reconsider j = i - (len f) as Element of NAT by INT_1:18;
A11: i <= len ((sqr f) ^ (sqr g)) by A1, A2, A3, A4, A6, FINSEQ_1:35;
thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i by RVSUM_1:def 8
.= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:23
.= sqrreal . (g . j) by A10, FINSEQ_1:37
.= (g . j) ^2 by RVSUM_1:def 2
.= (sqr g) . j by VALUED_1:11
.= ((sqr f) ^ (sqr g)) . i by A1, A10, A11, FINSEQ_1:37 ; :: thesis: verum

end;

end;

end;

hence sqr (f ^ g) = (sqr f) ^ (sqr g) by A5, FINSEQ_1:18; :: thesis: verum