per cases ( o2 = {} or o2 <> {} ) ;

suppose A1: o2 = {} ; :: thesis: ex b₁ being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b₁ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₁ . o = b . (o -^ o1) ) )

then reconsider a9 = a as Element of Bags (o1 +^ o2) by ORDINAL2:27;
take a9 ; :: thesis: for o being Ordinal holds
( ( o in o1 implies a9 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) ) )
let o be Ordinal; :: thesis: ( ( o in o1 implies a9 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) ) )
thus ( o in o1 implies a9 . o = a . o ) ; :: thesis: ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) )
o1 +^ o2 = o1 by A1, ORDINAL2:27;
hence ( o in (o1 +^ o2) \ o1 implies a9 . o = b . (o -^ o1) ) by XBOOLE_1:37; :: thesis: verum

end;

suppose o2 <> {} ; :: thesis: ex b₁ being Element of Bags (o1 +^ o2) st
for o being Ordinal holds
( ( o in o1 implies b₁ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₁ . o = b . (o -^ o1) ) )

then reconsider o29 = o2 as non empty Ordinal ;
defpred S₁[ object , object ] means ex o being Ordinal st
( o = $1 & ( o in o1 implies $2 = a . o ) & ( o in (o1 +^ o2) \ o1 implies $2 = b . (o -^ o1) ) );
deffunc H₁( Element of o29) -> set = o1 +^ $1;
set B = { H₁(o) where o is Element of o29 : o in support b } ;
set C = { (o1 +^ o) where o is Element of o29 : verum } ;
A2: for i being object st i in o1 +^ o2 holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in o1 +^ o2 implies ex j being object st S₁[i,j] )
assume A3: i in o1 +^ o2 ; :: thesis: ex j being object st S₁[i,j]
reconsider o = i as Ordinal by A3;
A4: ( o in o1 iff not o in (o1 +^ o2) \ o1 ) by A3, XBOOLE_0:def 5;

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

suppose A5: o in o1 ; :: thesis: ex j being object st S₁[i,j]

take a . o ; :: thesis: S₁[i,a . o]
take o ; :: thesis: ( o = i & ( o in o1 implies a . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a . o = b . (o -^ o1) ) )
thus ( o = i & ( o in o1 implies a . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a . o = b . (o -^ o1) ) ) by A5, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A6: o in (o1 +^ o2) \ o1 ; :: thesis: ex j being object st S₁[i,j]

take b . (o -^ o1) ; :: thesis: S₁[i,b . (o -^ o1)]
thus S₁[i,b . (o -^ o1)] by A4, A6; :: thesis: verum

end;

end;

end;

consider f being ManySortedSet of o1 +^ o2 such that
A7: for i being object st i in o1 +^ o2 holds
S₁[i,f . i] from PBOOLE:sch 3(A2);
A8: support f c= (support a) \/ { H₁(o) where o is Element of o29 : o in support b }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in (support a) \/ { H₁(o) where o is Element of o29 : o in support b } )
assume x in support f ; :: thesis: x in (support a) \/ { H₁(o) where o is Element of o29 : o in support b }
then A9: f . x <> 0 by PRE_POLY:def 7;
then x in dom f by FUNCT_1:def 2;
then A10: x in o1 +^ o2 by PARTFUN1:def 2;
for x being set holds
( x in { (o1 +^ o) where o is Element of o29 : verum } iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) )

proof

let x be set ; :: thesis: ( x in { (o1 +^ o) where o is Element of o29 : verum } iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) )
thus ( x in { (o1 +^ o) where o is Element of o29 : verum } implies ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ) :: thesis: ( ex o being Ordinal st
( x = o1 +^ o & o in o2 ) implies x in { (o1 +^ o) where o is Element of o29 : verum } )

proof

assume x in { (o1 +^ o) where o is Element of o29 : verum } ; :: thesis: ex o being Ordinal st
( x = o1 +^ o & o in o2 )
then ex o9 being Element of o29 st x = o1 +^ o9 ;
hence ex o being Ordinal st
( x = o1 +^ o & o in o2 ) ; :: thesis: verum

end;

thus ( ex o being Ordinal st
( x = o1 +^ o & o in o2 ) implies x in { (o1 +^ o) where o is Element of o29 : verum } ) ; :: thesis: verum

end;

then A11: x in o1 \/ { (o1 +^ o) where o is Element of o29 : verum } by A10, Th1;

per cases ( x in o1 or x in { (o1 +^ o) where o is Element of o29 : verum } ) by A11, XBOOLE_0:def 3;

suppose A12: x in o1 ; :: thesis: x in (support a) \/ { H₁(o) where o is Element of o29 : o in support b }

S₁[x,f . x] by A7, A10;
then x in support a by A9, A12, PRE_POLY:def 7;
hence x in (support a) \/ { H₁(o) where o is Element of o29 : o in support b } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in { (o1 +^ o) where o is Element of o29 : verum } ; :: thesis: x in (support a) \/ { H₁(o) where o is Element of o29 : o in support b }

then ex o9 being Element of o29 st x = o1 +^ o9 ;
then consider o99 being Ordinal such that
A13: x = o1 +^ o99 and
A14: o99 in o2 ;
reconsider o = x as Ordinal by A13;
A15: o1 c= o by A13, ORDINAL3:24;

A16: now :: thesis: not o in o1

per cases ( o = o1 or o <> o1 ) ;

suppose o = o1 ; :: thesis: not o in o1

hence not o in o1 ; :: thesis: verum

end;

suppose o <> o1 ; :: thesis: not o in o1

then o1 c< o by A15;
hence not o in o1 by ORDINAL1:11; :: thesis: verum

end;

end;

end;

A17: S₁[x,f . x] by A7, A10;
( x in o1 +^ o2 & o99 = o -^ o1 ) by A13, A14, ORDINAL2:32, ORDINAL3:52;
then o99 in support b by A9, A16, A17, PRE_POLY:def 7, XBOOLE_0:def 5;
then x in { H₁(o) where o is Element of o29 : o in support b } by A13;
hence x in (support a) \/ { H₁(o) where o is Element of o29 : o in support b } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A18: support b is finite ;
{ H₁(o) where o is Element of o29 : o in support b } is finite from FRAENKEL:sch 21(A18);
then A19: f is finite-support by A8, PRE_POLY:def 8;
f is natural-valued

proof

let x be object ; :: according to VALUED_0:def 12 :: thesis: ( not x in dom f or f . x is natural )
assume x in dom f ; :: thesis: f . x is natural
then A20: x in o1 +^ o2 by PARTFUN1:def 2;
then reconsider o = x as Ordinal ;
A21: ex o9 being Ordinal st
( o9 = x & ( o9 in o1 implies f . x = a . o9 ) & ( o9 in (o1 +^ o2) \ o1 implies f . x = b . (o9 -^ o1) ) ) by A7, A20;

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

suppose o in o1 ; :: thesis: f . x is natural

hence f . x is natural by A21; :: thesis: verum

end;

suppose o in (o1 +^ o2) \ o1 ; :: thesis: f . x is natural

hence f . x is natural by A21; :: thesis: verum

end;

end;

end;

then reconsider f = f as Element of Bags (o1 +^ o2) by A19, PRE_POLY:def 12;
take f ; :: thesis: for o being Ordinal holds
( ( o in o1 implies f . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies f . o = b . (o -^ o1) ) )
let o be Ordinal; :: thesis: ( ( o in o1 implies f . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies f . o = b . (o -^ o1) ) )
thus ( o in o1 implies f . o = a . o ) :: thesis: ( o in (o1 +^ o2) \ o1 implies f . o = b . (o -^ o1) )

proof

assume A22: o in o1 ; :: thesis: f . o = a . o
o1 c= o1 +^ o2 by ORDINAL3:24;
then ex p being Ordinal st
( p = o & ( p in o1 implies f . o = a . p ) & ( p in (o1 +^ o2) \ o1 implies f . o = b . (p -^ o1) ) ) by A7, A22;
hence f . o = a . o by A22; :: thesis: verum

end;

assume A23: o in (o1 +^ o2) \ o1 ; :: thesis: f . o = b . (o -^ o1)
then ex p being Ordinal st
( p = o & ( p in o1 implies f . o = a . p ) & ( p in (o1 +^ o2) \ o1 implies f . o = b . (p -^ o1) ) ) by A7;
hence f . o = b . (o -^ o1) by A23; :: thesis: verum

end;

end;