let o1, o2 be Ordinal; :: thesis: for a1, b1 being Element of Bags o1
for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
let a1, b1 be Element of Bags o1; :: thesis: for a2, b2 being Element of Bags o2 holds
( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
let a2, b2 be Element of Bags o2; :: thesis: ( a1 +^ a2 < b1 +^ b2 iff ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) )
thus ( not a1 +^ a2 < b1 +^ b2 or a1 < b1 or ( a1 = b1 & a2 < b2 ) ) :: thesis: ( ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) implies a1 +^ a2 < b1 +^ b2 )

proof

assume a1 +^ a2 < b1 +^ b2 ; :: thesis: ( a1 < b1 or ( a1 = b1 & a2 < b2 ) )
then consider k being Ordinal such that
A1: (a1 +^ a2) . k < (b1 +^ b2) . k and
A2: for l being Ordinal st l in k holds
(a1 +^ a2) . l = (b1 +^ b2) . l by PRE_POLY:def 9;

now

assume not k in dom (b1 +^ b2) ; :: thesis: contradiction
then (b1 +^ b2) . k = 0 by FUNCT_1:def 4;
hence contradiction by A1, NAT_1:2; :: thesis: verum

end;

then A3: k in o1 +^ o2 by PARTFUN1:def 4;

now

per cases ( k in o1 or k in (o1 +^ o2) \ o1 ) by A3, XBOOLE_0:def 5;

case A4: k in o1 ; :: thesis: a1 < b1

reconsider a1' = a1, b1' = b1 as bag of ;
A5: for l being Ordinal st l in k holds
a1' . l = b1' . l

proof

let l be Ordinal; :: thesis: ( l in k implies a1' . l = b1' . l )
assume A6: l in k ; :: thesis: a1' . l = b1' . l
then A7: (a1 +^ a2) . l = (b1 +^ b2) . l by A2;
A8: l in o1 by A4, A6, ORDINAL1:19;
then (a1 +^ a2) . l = a1 . l by Def1;
hence a1' . l = b1' . l by A7, A8, Def1; :: thesis: verum

end;

(a1 +^ a2) . k = a1 . k by A4, Def1;
then a1 . k < b1 . k by A1, A4, Def1;
hence a1 < b1 by A5, PRE_POLY:def 9; :: thesis: verum

end;

case A9: k in (o1 +^ o2) \ o1 ; :: thesis: ( a1 = b1 & a2 < b2 )

set k1 = k -^ o1;
not k in o1 by A9, XBOOLE_0:def 5;
then o1 c= k by ORDINAL1:26;
then A10: k = o1 +^ (k -^ o1) by ORDINAL3:def 6;
A11: for l being Ordinal st l in k -^ o1 holds
a2 . l = b2 . l

proof

let l be Ordinal; :: thesis: ( l in k -^ o1 implies a2 . l = b2 . l )
o1 c= o1 +^ l by ORDINAL3:27;
then A12: not o1 +^ l in o1 by ORDINAL1:7;
assume A13: l in k -^ o1 ; :: thesis: a2 . l = b2 . l
then o1 +^ l in o1 +^ (k -^ o1) by ORDINAL2:49;
then o1 +^ l in o1 +^ o2 by A9, A10, ORDINAL1:19;
then A14: o1 +^ l in (o1 +^ o2) \ o1 by A12, XBOOLE_0:def 5;
then A15: (b1 +^ b2) . (o1 +^ l) = b2 . ((o1 +^ l) -^ o1) by Def1
.= b2 . l by ORDINAL3:65 ;
(a1 +^ a2) . (o1 +^ l) = a2 . ((o1 +^ l) -^ o1) by A14, Def1
.= a2 . l by ORDINAL3:65 ;
hence a2 . l = b2 . l by A2, A10, A13, A15, ORDINAL2:49; :: thesis: verum

end;

for i being set st i in o1 holds
a1 . i = b1 . i

proof

not k in o1 by A9, XBOOLE_0:def 5;
then A16: o1 c= k by ORDINAL1:26;
let i be set ; :: thesis: ( i in o1 implies a1 . i = b1 . i )
assume A17: i in o1 ; :: thesis: a1 . i = b1 . i
then reconsider i' = i as Ordinal ;
( (a1 +^ a2) . i' = a1 . i' & (b1 +^ b2) . i' = b1 . i' ) by A17, Def1;
hence a1 . i = b1 . i by A2, A17, A16; :: thesis: verum

end;

hence a1 = b1 by PBOOLE:3; :: thesis: a2 < b2
(a1 +^ a2) . k = a2 . (k -^ o1) by A9, Def1;
then a2 . (k -^ o1) < b2 . (k -^ o1) by A1, A9, Def1;
hence a2 < b2 by A11, PRE_POLY:def 9; :: thesis: verum

end;

end;

end;

hence ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) ; :: thesis: verum

end;

thus ( ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) implies a1 +^ a2 < b1 +^ b2 ) :: thesis: verum

proof

assume A18: ( a1 < b1 or ( a1 = b1 & a2 < b2 ) ) ; :: thesis: a1 +^ a2 < b1 +^ b2

now

per cases ( a1 < b1 or not a1 < b1 ) ;

case a1 < b1 ; :: thesis: a1 +^ a2 < b1 +^ b2

then consider k being Ordinal such that
A19: k in o1 and
A20: a1 . k < b1 . k and
A21: for l being Ordinal st l in k holds
a1 . l = b1 . l by Th2;
A22: for l being Ordinal st l in k holds
(a1 +^ a2) . l = (b1 +^ b2) . l

proof

let l be Ordinal; :: thesis: ( l in k implies (a1 +^ a2) . l = (b1 +^ b2) . l )
assume A23: l in k ; :: thesis: (a1 +^ a2) . l = (b1 +^ b2) . l
then l in o1 by A19, ORDINAL1:19;
then ( (a1 +^ a2) . l = a1 . l & (b1 +^ b2) . l = b1 . l ) by Def1;
hence (a1 +^ a2) . l = (b1 +^ b2) . l by A21, A23; :: thesis: verum

end;

( (a1 +^ a2) . k = a1 . k & (b1 +^ b2) . k = b1 . k ) by A19, Def1;
hence a1 +^ a2 < b1 +^ b2 by A20, A22, PRE_POLY:def 9; :: thesis: verum

end;

case A24: not a1 < b1 ; :: thesis: a1 +^ a2 < b1 +^ b2

then consider k being Ordinal such that
A25: k in o2 and
A26: a2 . k < b2 . k and
A27: for l being Ordinal st l in k holds
a2 . l = b2 . l by A18, Th2;
set x = o1 +^ k;
A28: for l being Ordinal st l in o1 +^ k holds
(a1 +^ a2) . l = (b1 +^ b2) . l

proof

let l be Ordinal; :: thesis: ( l in o1 +^ k implies (a1 +^ a2) . l = (b1 +^ b2) . l )
assume A29: l in o1 +^ k ; :: thesis: (a1 +^ a2) . l = (b1 +^ b2) . l

per cases ( l in o1 or not l in o1 ) ;

suppose A30: l in o1 ; :: thesis: (a1 +^ a2) . l = (b1 +^ b2) . l

hence (a1 +^ a2) . l = b1 . l by A18, A24, Def1
.= (b1 +^ b2) . l by A30, Def1 ;
:: thesis: verum

end;

suppose A31: not l in o1 ; :: thesis: (a1 +^ a2) . l = (b1 +^ b2) . l

then o1 c= l by ORDINAL1:26;
then l -^ o1 in (o1 +^ k) -^ o1 by A29, ORDINAL3:66;
then A32: l -^ o1 in k by ORDINAL3:65;
o1 +^ k in o1 +^ o2 by A25, ORDINAL2:49;
then l in o1 +^ o2 by A29, ORDINAL1:19;
then A33: l in (o1 +^ o2) \ o1 by A31, XBOOLE_0:def 5;
hence (a1 +^ a2) . l = a2 . (l -^ o1) by Def1
.= b2 . (l -^ o1) by A27, A32
.= (b1 +^ b2) . l by A33, Def1 ;
:: thesis: verum

end;

end;

end;

o1 c= o1 +^ k by ORDINAL3:27;
then A34: not o1 +^ k in o1 by ORDINAL1:7;
A35: k = (o1 +^ k) -^ o1 by ORDINAL3:65;
o1 +^ k in o1 +^ o2 by A25, ORDINAL2:49;
then A36: o1 +^ k in (o1 +^ o2) \ o1 by A34, XBOOLE_0:def 5;
then (b1 +^ b2) . (o1 +^ k) = b2 . ((o1 +^ k) -^ o1) by Def1;
then (a1 +^ a2) . (o1 +^ k) < (b1 +^ b2) . (o1 +^ k) by A26, A36, A35, Def1;
hence a1 +^ a2 < b1 +^ b2 by A28, PRE_POLY:def 9; :: thesis: verum

end;

end;

end;

hence a1 +^ a2 < b1 +^ b2 ; :: thesis: verum

end;