let f, h, g, 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:35;
A4: len (h ^ k) = (len h) + (len k) by FINSEQ_1:35;
A5: len (abs ((f ^ g) + (h ^ k))) = len ((f ^ g) + (h ^ k)) by Th10
.= len (f ^ g) by A1, A2, A3, A4, Th7
.= (len (f + h)) + (len g) by A1, A3, Th7
.= (len (f + h)) + (len (g + k)) by A2, Th7
.= (len (abs (f + h))) + (len (g + k)) by Th10
.= (len (abs (f + h))) + (len (abs (g + k))) by Th10
.= len ((abs (f + h)) ^ (abs (g + k))) by FINSEQ_1:35 ;
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 13;
A8: i in dom (abs ((f ^ g) + (h ^ k))) by A6, A7, FINSEQ_3:27;
then A9: i in dom ((f ^ g) + (h ^ k)) by Th10;

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:31;
A12: i in dom (f + h) by A1, A10, Th7;
then A13: i in dom (abs (f + h)) by Th10;
thus (abs ((f ^ g) + (h ^ k))) . i = abs (((f ^ g) + (h ^ k)) . i1) by A8, TOPREAL6:17
.= abs (((f ^ g) . i) + ((h ^ k) . i)) by A9, VALUED_1:def 1
.= abs ((f . i) + ((h ^ k) . i)) by A10, FINSEQ_1:def 7
.= abs ((f . i) + (h . i)) by A11, FINSEQ_1:def 7
.= abs ((f + h) . i1) by A12, VALUED_1:def 1
.= (abs (f + h)) . i1 by A13, TOPREAL6:17
.= ((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:27;
then reconsider j = i - (len f) as Element of NAT by INT_1:18;
A15: len (f + h) < i by A1, A14, Th7;
then A16: len (abs (f + h)) < i by Th10;
i <= len ((f ^ g) + (h ^ k)) by A7, Th10;
then A17: i <= len (f ^ g) by A1, A2, A3, A4, Th7;
then i <= (len (f + h)) + (len g) by A1, A3, Th7;
then i <= (len (f + h)) + (len (g + k)) by A2, Th7;
then i - (len (f + h)) in dom (g + k) by A15, Th5;
then A18: j in dom (g + k) by A1, Th7;
then A19: j in dom (abs (g + k)) by Th10;
len f = len (f + h) by A1, Th7;
then A20: j = i - (len (abs (f + h))) by Th10;
thus (abs ((f ^ g) + (h ^ k))) . i = abs (((f ^ g) + (h ^ k)) . i1) by A8, TOPREAL6:17
.= abs (((f ^ g) . i) + ((h ^ k) . i)) by A9, VALUED_1:def 1
.= abs ((g . j) + ((h ^ k) . i)) by A14, A17, FINSEQ_1:37
.= abs ((g . j) + (k . j)) by A1, A2, A3, A4, A14, A17, FINSEQ_1:37
.= abs ((g + k) . j) by A18, VALUED_1:def 1
.= (abs (g + k)) . j by A19, TOPREAL6:17
.= ((abs (f + h)) ^ (abs (g + k))) . i by A5, A7, A16, A20, FINSEQ_1:37 ; :: thesis: verum

end;

end;

end;

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