let f, g, h, k be FinSequence of REAL ; :: thesis: ( len f = len h & len g = len k implies abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k)) )
assume that
A1: len f = len h and
A2: len g = len k ; :: thesis: abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (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 (abs ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th9
.= 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 (abs (f + h))) + (len (g + k)) by Th9
.= (len (abs (f + h))) + (len (abs (g + k))) by Th9
.= len ((abs (f + h)) ^ (abs (g + k))) by FINSEQ_1:22 ;
for i being Nat st 1 <= i & i <= len (abs ((f ^ g) + (h ^ k))) holds
(abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (abs ((f ^ g) + (h ^ k))) implies (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i )
assume that
A6: 1 <= i and
A7: i <= len (abs ((f ^ g) + (h ^ k))) ; :: thesis: (abs ((f ^ g) + (h ^ k))) . i = ((abs (f + h)) ^ (abs (g + k))) . i
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A8: i in dom (abs ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:25;
then A9: i in dom ((f ^ g) + (h ^ k)) by Th9;

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

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

then A11: i in dom h by A1, FINSEQ_3:29;
A12: i in dom (f + h) by A1, A10, Th6;
then A13: i in dom (abs (f + h)) by Th9;
thus (abs ((f ^ g) + (h ^ k))) . i = |.(((f ^ g) + (h ^ k)) . i1).| by A8, TOPREAL6:12
.= |.(((f ^ g) . i) + ((h ^ k) . i)).| by A9, VALUED_1:def 1
.= |.((f . i) + ((h ^ k) . i)).| by A10, FINSEQ_1:def 7
.= |.((f . i) + (h . i)).| by A11, FINSEQ_1:def 7
.= |.((f + h) . i1).| by A12, VALUED_1:def 1
.= (abs (f + h)) . i1 by A13, TOPREAL6:12
.= ((abs (f + h)) ^ (abs (g + k))) . i by A13, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

then A14: len f < i by A6, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A15: len (f + h) < i by A1, A14, Th6;
then A16: len (abs (f + h)) < i by Th9;
i <= len ((f ^ g) + (h ^ k)) by A7, Th9;
then A17: 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 A15, Th4;
then A18: j in dom (g + k) by A1, Th6;
then A19: j in dom (abs (g + k)) by Th9;
len f = len (f + h) by A1, Th6;
then A20: j = i - (len (abs (f + h))) by Th9;
thus (abs ((f ^ g) + (h ^ k))) . i = |.(((f ^ g) + (h ^ k)) . i1).| by A8, TOPREAL6:12
.= |.(((f ^ g) . i) + ((h ^ k) . i)).| by A9, VALUED_1:def 1
.= |.((g . j) + ((h ^ k) . i)).| by A14, A17, FINSEQ_1:24
.= |.((g . j) + (k . j)).| by A1, A2, A3, A4, A14, A17, FINSEQ_1:24
.= |.((g + k) . j).| by A18, VALUED_1:def 1
.= (abs (g + k)) . j by A19, TOPREAL6:12
.= ((abs (f + h)) ^ (abs (g + k))) . i by A5, A7, A16, A20, FINSEQ_1:24 ; :: thesis: verum

end;

end;

end;

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