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 A2: o1 +^ o2 = o1 by ORDINAL2:44;
reconsider a' = a as Element of Bags (o1 +^ o2) by A1, ORDINAL2:44;
take a' ; :: thesis: for o being Ordinal holds
( ( o in o1 implies a' . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a' . o = b . (o -^ o1) ) )
let o be Ordinal; :: thesis: ( ( o in o1 implies a' . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a' . o = b . (o -^ o1) ) )
thus ( o in o1 implies a' . o = a . o ) ; :: thesis: ( o in (o1 +^ o2) \ o1 implies a' . o = b . (o -^ o1) )
thus ( o in (o1 +^ o2) \ o1 implies a' . o = b . (o -^ o1) ) by A2, 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 o2' = o2 as non empty Ordinal ;
defpred S₁[ set , set ] 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) ) );
A3: for i being set st i in o1 +^ o2 holds
ex j being set st S₁[i,j]

proof

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

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

suppose A6: o in o1 ; :: thesis: ex j being set 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 A6, XBOOLE_0:def 5; :: thesis: verum

end;

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

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

end;

end;

end;

consider f being ManySortedSet of such that
A8: for i being set st i in o1 +^ o2 holds
S₁[i,f . i] from PBOOLE:sch 3(A3);
A9: f is natural-valued

proof

let x be set ; :: 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 A10: x in o1 +^ o2 by PARTFUN1:def 4;
then reconsider o = x as Ordinal ;
consider o' being Ordinal such that
A11: ( o' = x & ( o' in o1 implies f . x = a . o' ) & ( o' in (o1 +^ o2) \ o1 implies f . x = b . (o' -^ o1) ) ) by A8, A10;

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

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

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

end;

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

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

end;

end;

end;

deffunc H₁( Element of o2') -> set = o1 +^ $1;
set B = { H₁(o) where o is Element of o2' : o in support b } ;
set C = { (o1 +^ o) where o is Element of o2' : verum } ;
A12: support f c= (support a) \/ { H₁(o) where o is Element of o2' : o in support b }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in (support a) \/ { H₁(o) where o is Element of o2' : o in support b } )
assume x in support f ; :: thesis: x in (support a) \/ { H₁(o) where o is Element of o2' : o in support b }
then A13: f . x <> 0 by POLYNOM1:def 7;
then x in dom f by FUNCT_1:def 4;
then A14: x in o1 +^ o2 by PARTFUN1:def 4;
for x being set holds
( x in { (o1 +^ o) where o is Element of o2' : 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 o2' : verum } iff ex o being Ordinal st
( x = o1 +^ o & o in o2 ) )
thus ( x in { (o1 +^ o) where o is Element of o2' : 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 o2' : verum } )

proof

assume x in { (o1 +^ o) where o is Element of o2' : verum } ; :: thesis: ex o being Ordinal st
( x = o1 +^ o & o in o2 )
then ex o' being Element of o2' st x = o1 +^ o' ;
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 o2' : verum } ) ; :: thesis: verum

end;

then A15: x in o1 \/ { (o1 +^ o) where o is Element of o2' : verum } by A14, Th1;

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

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

S₁[x,f . x] by A8, A14;
then x in support a by A13, A16, POLYNOM1:def 7;
hence x in (support a) \/ { H₁(o) where o is Element of o2' : o in support b } by XBOOLE_0:def 3; :: thesis: verum

end;

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

then ex o' being Element of o2' st x = o1 +^ o' ;
then consider o'' being Ordinal such that
A17: ( x = o1 +^ o'' & o'' in o2 ) ;
A18: x in o1 +^ o2 by A17, ORDINAL2:49;
reconsider o = x as Ordinal by A17;
A19: o1 c= o by A17, ORDINAL3:27;

A20: now

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 A19, XBOOLE_0:def 8;
hence not o in o1 by ORDINAL1:21; :: thesis: verum

end;

end;

end;

A21: S₁[x,f . x] by A8, A14;
o'' = o -^ o1 by A17, ORDINAL3:65;
then o'' in support b by A13, A18, A20, A21, POLYNOM1:def 7, XBOOLE_0:def 5;
then x in { H₁(o) where o is Element of o2' : o in support b } by A17;
hence x in (support a) \/ { H₁(o) where o is Element of o2' : o in support b } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

A22: support b is finite ;
{ H₁(o) where o is Element of o2' : o in support b } is finite from FRAENKEL:sch 21(A22);
then (support a) \/ { H₁(o) where o is Element of o2' : o in support b } is finite ;
then support f is finite by A12;
then f is finite-support by POLYNOM1:def 8;
then reconsider f = f as Element of Bags (o1 +^ o2) by A9, POLYNOM1:def 14;
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 A23: o in o1 ; :: thesis: f . o = a . o
o1 c= o1 +^ o2 by ORDINAL3:27;
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 A8, A23;
hence f . o = a . o by A23; :: thesis: verum

end;

assume A24: 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 A8;
hence f . o = b . (o -^ o1) by A24; :: thesis: verum

end;

end;