let A be finite Ordinal-Sequence; :: thesis: for a being Ordinal holds Sum^ (A | a) c= Sum^ A
let a be Ordinal; :: thesis: Sum^ (A | a) c= Sum^ A

per cases ( dom A c= a or a c= dom A ) ;

suppose dom A c= a ; :: thesis: Sum^ (A | a) c= Sum^ A

hence Sum^ (A | a) c= Sum^ A by RELAT_1:68; :: thesis: verum

end;

suppose A1: a c= dom A ; :: thesis: Sum^ (A | a) c= Sum^ A

then reconsider a = a as finite Ordinal ;
consider f1 being Ordinal-Sequence such that
A2: ( Sum^ (A | a) = last f1 & dom f1 = succ (dom (A | a)) & f1 . 0 = 0 ) and
A3: for n being Nat st n in dom (A | a) holds
f1 . (n + 1) = (f1 . n) +^ ((A | a) . n) by ORDINAL5:def 8;
consider f2 being Ordinal-Sequence such that
A4: ( Sum^ A = last f2 & dom f2 = succ (dom A) & f2 . 0 = 0 ) and
A5: for n being Nat st n in dom A holds
f2 . (n + 1) = (f2 . n) +^ (A . n) by ORDINAL5:def 8;
defpred S₁[ Nat] means ( $1 in dom f1 implies f1 . $1 = f2 . $1 );
A6: S₁[ 0 ] by A2, A4;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
assume n + 1 in dom f1 ; :: thesis: f1 . (n + 1) = f2 . (n + 1)
then A9: succ n in dom f1 by Lm5;
n in succ n by ORDINAL1:6;
then A10: f1 . n = f2 . n by A8, A9, ORDINAL1:10;
A11: n in dom (A | a) by A2, A9, ORDINAL3:3;
then A12: n in dom A by RELAT_1:57;
thus f1 . (n + 1) = (f1 . n) +^ ((A | a) . n) by A3, A11
.= (f2 . n) +^ (A . n) by A10, A11, FUNCT_1:47
.= f2 . (n + 1) by A5, A12 ; :: thesis: verum

end;

A13: for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
A14: ( last f1 = f1 . (dom (A | a)) & last f2 = f2 . (dom A) ) by A2, A4, ORDINAL2:6;
then A15: last f1 = f2 . (dom (A | a)) by A2, A13, ORDINAL1:6
.= f2 . a by A1, RELAT_1:62 ;
Segm a c= Segm (dom A) by A1;
then consider k being Nat such that
A16: dom A = a + k by NAT_1:10, NAT_1:39;
defpred S₂[ Nat] means ( a + $1 <= dom A implies f2 . a c= f2 . (a + $1) );
A17: S₂[ 0 ] ;
A18: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A19: S₂[n] ; :: thesis: S₂[n + 1]
assume A20: a + (n + 1) <= dom A ; :: thesis: f2 . a c= f2 . (a + (n + 1))
then (a + n) + 1 < (dom A) + 1 by NAT_1:13;
then A21: f2 . a c= f2 . (a + n) by A19, XREAL_1:6;
Segm (a + (n + 1)) c= Segm (dom A) by A20, NAT_1:39;
then (a + n) + 1 c= dom A ;
then succ (a + n) c= dom A by Lm5;
then f2 . ((a + n) + 1) = (f2 . (a + n)) +^ (A . (a + n)) by A5, ORDINAL1:21;
then f2 . (a + n) c= f2 . ((a + n) + 1) by ORDINAL3:24;
hence f2 . a c= f2 . (a + (n + 1)) by A21, XBOOLE_1:1; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A17, A18);
hence Sum^ (A | a) c= Sum^ A by A2, A4, A14, A15, A16; :: thesis: verum

end;

end;