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

hence abs (f ^ g) = (abs f) ^ (abs g) by A4, FINSEQ_1:14; :: thesis: verum

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

len (abs (f ^ g)) = len ((abs f) ^ (abs g))
by A3, A1, A2, FINSEQ_1:22;
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;

end;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 )
;

end;

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

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

hence abs (f ^ g) = (abs f) ^ (abs g) by A4, FINSEQ_1:14; :: thesis: verum