let A, B be finite Ordinal-Sequence; ( dom A c= dom B & ( for a being object st a in dom A holds
A . a c= B . a ) implies Sum^ A c= Sum^ B )
assume that
A1:
dom A c= dom B
and
A2:
for a being object st a in dom A holds
A . a c= B . a
; Sum^ A c= Sum^ B
set a = dom A;
consider f1 being Ordinal-Sequence such that
A3:
( Sum^ A = last f1 & dom f1 = succ (dom A) & f1 . 0 = 0 )
and
A4:
for n being Nat st n in dom A holds
f1 . (n + 1) = (f1 . n) +^ (A . n)
by ORDINAL5:def 8;
consider f2 being Ordinal-Sequence such that
A5:
( Sum^ (B | (dom A)) = last f2 & dom f2 = succ (dom (B | (dom A))) & f2 . 0 = 0 )
and
A6:
for n being Nat st n in dom (B | (dom A)) holds
f2 . (n + 1) = (f2 . n) +^ ((B | (dom A)) . n)
by ORDINAL5:def 8;
defpred S1[ Nat] means ( $1 in succ (dom A) implies f1 . $1 c= f2 . $1 );
A7:
S1[ 0 ]
by A3;
A8:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A9:
S1[
n]
;
S1[n + 1]
assume
n + 1
in succ (dom A)
;
f1 . (n + 1) c= f2 . (n + 1)
then A10:
succ n in succ (dom A)
by Lm5;
then A11:
n in dom A
by ORDINAL3:3;
n in succ n
by ORDINAL1:6;
then A12:
f1 . n c= f2 . n
by A9, A10, ORDINAL1:10;
A13:
f1 . (n + 1) = (f1 . n) +^ (A . n)
by A4, A10, ORDINAL3:3;
A14:
n in dom (B | (dom A))
by A1, A11, RELAT_1:62;
then A15:
f2 . (n + 1) =
(f2 . n) +^ ((B | (dom A)) . n)
by A6
.=
(f2 . n) +^ (B . n)
by A14, FUNCT_1:47
;
A . n c= B . n
by A2, A10, ORDINAL3:3;
hence
f1 . (n + 1) c= f2 . (n + 1)
by A12, A13, A15, ORDINAL3:18;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A8);
then
f1 . (dom A) c= f2 . (dom A)
by ORDINAL1:6;
then
last f1 c= f2 . (dom A)
by A3, ORDINAL2:6;
then
last f1 c= f2 . (dom (B | (dom A)))
by A1, RELAT_1:62;
then A17:
Sum^ A c= Sum^ (B | (dom A))
by A3, A5, ORDINAL2:6;
Sum^ (B | (dom A)) c= Sum^ B
by Th27;
hence
Sum^ A c= Sum^ B
by A17, XBOOLE_1:1; verum