let A, B be finite Ordinal-Sequence; :: thesis: ( 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 ; :: thesis: 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 S₁[ Nat] means ( $1 in succ (dom A) implies f1 . $1 c= f2 . $1 );
A7: S₁[ 0 ] by A3;
A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
assume n + 1 in succ (dom A) ; :: thesis: 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; :: thesis: verum

end;

for n being Nat holds S₁[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; :: thesis: verum