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 POLYNOM1:def 11;

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

then (a1 +^ a2) . k = a1 . k by Def1;
then A5: a1 . k < b1 . k by A1, A4, Def1;
reconsider a1' = a1, b1' = b1 as bag of ;
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;

hence a1 < b1 by A5, POLYNOM1:def 11; :: thesis: verum

end;

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

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

proof

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

end;

hence a1 = b1 by PBOOLE:3; :: thesis: a2 < b2
not k in o1 by A9, XBOOLE_0:def 5;
then o1 c= k by ORDINAL1:26;
then A13: k = o1 +^ (k -^ o1) by ORDINAL3:def 6;
set k1 = k -^ o1;
(a1 +^ a2) . k = a2 . (k -^ o1) by A9, Def1;
then A14: a2 . (k -^ o1) < b2 . (k -^ o1) by A1, A9, Def1;
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 )
assume A15: l in k -^ o1 ; :: thesis: a2 . l = b2 . l
then o1 +^ l in o1 +^ (k -^ o1) by ORDINAL2:49;
then A16: o1 +^ l in o1 +^ o2 by A9, A13, ORDINAL1:19;
o1 c= o1 +^ l by ORDINAL3:27;
then not o1 +^ l in o1 by ORDINAL1:7;
then A17: o1 +^ l in (o1 +^ o2) \ o1 by A16, XBOOLE_0:def 5;
then A18: (a1 +^ a2) . (o1 +^ l) = a2 . ((o1 +^ l) -^ o1) by Def1
.= a2 . l by ORDINAL3:65 ;
(b1 +^ b2) . (o1 +^ l) = b2 . ((o1 +^ l) -^ o1) by A17, Def1
.= b2 . l by ORDINAL3:65 ;
hence a2 . l = b2 . l by A2, A13, A15, A18, ORDINAL2:49; :: thesis: verum

end;

hence a2 < b2 by A14, POLYNOM1:def 11; :: 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 A19: ( 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
A20: k in o1 and
A21: a1 . k < b1 . k and
A22: for l being Ordinal st l in k holds
a1 . l = b1 . l by Th2;
A23: (a1 +^ a2) . k = a1 . k by A20, Def1;
A24: (b1 +^ b2) . k = b1 . k by A20, Def1;
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 A25: l in k ; :: thesis: (a1 +^ a2) . l = (b1 +^ b2) . l
then A26: l in o1 by A20, ORDINAL1:19;
then A27: (a1 +^ a2) . l = a1 . l by Def1;
(b1 +^ b2) . l = b1 . l by A26, Def1;
hence (a1 +^ a2) . l = (b1 +^ b2) . l by A22, A25, A27; :: thesis: verum

end;

hence a1 +^ a2 < b1 +^ b2 by A21, A23, A24, POLYNOM1:def 11; :: thesis: verum

end;

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

then consider k being Ordinal such that
A29: k in o2 and
A30: a2 . k < b2 . k and
A31: for l being Ordinal st l in k holds
a2 . l = b2 . l by A19, Th2;
set x = o1 +^ k;
A32: o1 +^ k in o1 +^ o2 by A29, ORDINAL2:49;
o1 c= o1 +^ k by ORDINAL3:27;
then not o1 +^ k in o1 by ORDINAL1:7;
then A33: o1 +^ k in (o1 +^ o2) \ o1 by A32, XBOOLE_0:def 5;
then A34: (b1 +^ b2) . (o1 +^ k) = b2 . ((o1 +^ k) -^ o1) by Def1;
k = (o1 +^ k) -^ o1 by ORDINAL3:65;
then A35: (a1 +^ a2) . (o1 +^ k) < (b1 +^ b2) . (o1 +^ k) by A30, A33, A34, Def1;
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 A36: l in o1 +^ k ; :: thesis: (a1 +^ a2) . l = (b1 +^ b2) . l

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

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

hence (a1 +^ a2) . l = b1 . l by A19, A28, Def1
.= (b1 +^ b2) . l by A37, Def1 ;
:: thesis: verum

end;

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

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

end;

end;

end;

hence a1 +^ a2 < b1 +^ b2 by A35, POLYNOM1:def 11; :: thesis: verum

end;

end;

end;

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

end;