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

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (abs (f ^ g)) implies (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i )
assume that
A5: 1 <= i and
A6: i <= len (abs (f ^ g)) ; :: thesis: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
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: (abs (f ^ g)) . i = ((abs f) ^ (abs g)) . i

then A9: i in dom (abs f) by Th9;
thus (abs (f ^ g)) . i = absreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= absreal . (f . i) by A8, FINSEQ_1:def 7
.= |.(f . i1).| by EUCLID:def 2
.= (abs f) . i1 by A9, TOPREAL6:12
.= ((abs f) ^ (abs g)) . i by A9, FINSEQ_1:def 7 ; :: thesis: verum

end;

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

then A10: len f < i by A5, FINSEQ_3:25;
then reconsider j = i1 - (len f) as Element of NAT by INT_1:5;
A11: i <= len (f ^ g) by A6, Th9;
then A12: j in dom (abs g) by A1, A10, Th4;
A13: i <= len ((abs f) ^ (abs g)) by A3, A1, A2, A6, FINSEQ_1:22;
thus (abs (f ^ g)) . i = absreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= absreal . (g . j) by A10, A11, FINSEQ_1:24
.= |.(g . j).| by EUCLID:def 2
.= (abs g) . j by A12, TOPREAL6:12
.= ((abs f) ^ (abs g)) . i by A3, A10, A13, FINSEQ_1:24 ; :: thesis: verum

end;

end;

end;

len (abs (f ^ g)) = len ((abs f) ^ (abs g)) by A3, A1, A2, FINSEQ_1:22;
hence abs (f ^ g) = (abs f) ^ (abs g) by A4, FINSEQ_1:14; :: thesis: verum