let f, g be FinSequence of REAL ; 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;
( 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))
;
(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
not
i in dom f
;
(abs (f ^ g)) . i = ((abs f) ^ (abs g)) . ithen 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
;
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; verum