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, 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 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
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

reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A11: i in dom h by A1, A10, FINSEQ_3:29;
A12: i in dom (f - h) by A1, A10, Th7;
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:13
.= |.((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:13
.= (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 A14: not i in dom f ; :: 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;
A15: len f < i by A6, A14, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A16: len (f - h) < i by A1, A15, Th7;
then A17: len (abs (f - h)) < i by Th9;
i <= len ((f ^ g) - (h ^ k)) by A7, Th9;
then A18: 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 A16, Th4;
then A19: j in dom (g - k) by A1, Th7;
then A20: j in dom (abs (g - k)) by Th9;
len f = len (f - h) by A1, Th7;
then A21: 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:13
.= |.((g . j) - ((h ^ k) . i)).| by A15, A18, FINSEQ_1:24
.= |.((g . j) - (k . j)).| by A1, A2, A3, A4, A15, A18, FINSEQ_1:24
.= |.((g - k) . j).| by A19, VALUED_1:13
.= (abs (g - k)) . j by A20, TOPREAL6:12
.= ((abs (f - h)) ^ (abs (g - k))) . i by A5, A7, A17, A21, 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