let f, g be real-valued FinSequence; :: thesis: sqr (f ^ g) = (sqr f) ^ (sqr g)
A1: len f = len (sqr f) by Th143;
A2: len (sqr (f ^ g)) = len (f ^ g) by Th143;
A3: ( len g = len (sqr g) & len (f ^ g) = (len f) + (len g) ) by Th143, FINSEQ_1:22;
A4: 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 that
A5: 1 <= i and
A6: i <= len (sqr (f ^ g)) ; :: thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i
A7: i in dom (f ^ g) by A2, A5, A6, FINSEQ_3:25;
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 Th143;
thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i
.= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= sqrreal . (f . i) by A8, FINSEQ_1:def 7
.= (f . i) ^2 by Def2
.= (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 by A5, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A11: i <= len (f ^ g) by A6, Th143;
A12: i <= len ((sqr f) ^ (sqr g)) by A1, A3, A2, A6, FINSEQ_1:22;
thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i
.= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= sqrreal . (g . j) by A10, A11, FINSEQ_1:24
.= (g . j) ^2 by Def2
.= (sqr g) . j by VALUED_1:11
.= ((sqr f) ^ (sqr g)) . i by A1, A10, A12, FINSEQ_1:24 ; :: thesis: verum
end;
end;
end;
len (sqr (f ^ g)) = len ((sqr f) ^ (sqr g)) by A1, A3, A2, FINSEQ_1:22;
hence sqr (f ^ g) = (sqr f) ^ (sqr g) by A4; :: thesis: verum