let o1, o2 be Ordinal; :: thesis: for c being Element of Bags (o1 +^ o2) ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2
let c be Element of Bags (o1 +^ o2); :: thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2

per cases ( o2 is empty or not o2 is empty ) ;

suppose A1: o2 is empty ; :: thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2

then reconsider c2 = {} as Element of Bags o2 by PRE_POLY:51, TARSKI:def 1;
reconsider c1 = c as Element of Bags o1 by A1, ORDINAL2:27;
take c1 ; :: thesis: ex c2 being Element of Bags o2 st c = c1 +^ c2
take c2 ; :: thesis: c = c1 +^ c2
thus c = c1 +^ c2 by A1, Th3; :: thesis: verum

end;

suppose A2: not o2 is empty ; :: thesis: ex c1 being Element of Bags o1 ex c2 being Element of Bags o2 st c = c1 +^ c2

then reconsider o29 = o2 as non empty Ordinal ;
A3: support (c | o1) c= support c

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (c | o1) or x in support c )
assume x in support (c | o1) ; :: thesis: x in support c
then A4: (c | o1) . x <> 0 by PRE_POLY:def 7;
then x in dom (c | o1) by FUNCT_1:def 2;
then [x,((c | o1) . x)] in c | o1 by FUNCT_1:1;
then [x,((c | o1) . x)] in c by RELAT_1:def 11;
then (c | o1) . x = c . x by FUNCT_1:1;
hence x in support c by A4, PRE_POLY:def 7; :: thesis: verum

end;

dom c = o1 +^ o2 by PARTFUN1:def 2;
then o1 c= dom c by ORDINAL3:24;
then dom (c | o1) = o1 by RELAT_1:62;
then c | o1 is bag of o1 by A3, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;
then reconsider c1 = c | o1 as Element of Bags o1 by PRE_POLY:def 12;
deffunc H₁( Element of o1 +^ o29) -> set = $1 -^ o1;
defpred S₁[ object , object ] means for x1 being Element of o2 st x1 = $1 holds
$2 = c . (o1 +^ x1);
take c1 ; :: thesis: ex c2 being Element of Bags o2 st c = c1 +^ c2
set B = { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } ;
set C = { H₁(o9) where o9 is Element of o1 +^ o29 : o9 in support c } ;
A5: { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } c= { H₁(o9) where o9 is Element of o1 +^ o29 : o9 in support c }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } or x in { H₁(o9) where o9 is Element of o1 +^ o29 : o9 in support c } )
assume x in { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } ; :: thesis: x in { H₁(o9) where o9 is Element of o1 +^ o29 : o9 in support c }
then ex o9 being Element of o1 +^ o29 st
( x = o9 -^ o1 & o1 c= o9 & o9 in support c ) ;
hence x in { H₁(o9) where o9 is Element of o1 +^ o29 : o9 in support c } ; :: thesis: verum

end;

A6: for i being object st i in o2 holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in o2 implies ex j being object st S₁[i,j] )
assume i in o2 ; :: thesis: ex j being object st S₁[i,j]
then reconsider x1 = i as Element of o2 ;
take c . (o1 +^ x1) ; :: thesis: S₁[i,c . (o1 +^ x1)]
thus S₁[i,c . (o1 +^ x1)] ; :: thesis: verum

end;

consider f being ManySortedSet of o2 such that
A7: for i being object st i in o2 holds
S₁[i,f . i] from PBOOLE:sch 3(A6);
A8: support f c= { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } )
assume x in support f ; :: thesis: x in { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) }
then A9: f . x <> 0 by PRE_POLY:def 7;
then x in dom f by FUNCT_1:def 2;
then reconsider o9 = x as Element of o29 by PARTFUN1:def 2;
c . (o1 +^ o9) <> 0 by A7, A9;
then A10: o1 +^ o9 in support c by PRE_POLY:def 7;
reconsider o99 = o1 +^ o9 as Element of o1 +^ o29 by ORDINAL2:32;
( o9 = o99 -^ o1 & o1 c= o99 ) by ORDINAL3:24, ORDINAL3:52;
hence x in { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } by A10; :: thesis: verum

end;

A11: 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 A12: x in dom f ; :: thesis: f . x is natural
then reconsider o = x as Element of o2 by PARTFUN1:def 2;
x in o2 by A12, PARTFUN1:def 2;
then f . x = c . (o1 +^ o) by A7;
hence f . x is natural ; :: thesis: verum

end;

A13: support c is finite ;
{ H₁(o9) where o9 is Element of o1 +^ o29 : o9 in support c } is finite from FRAENKEL:sch 21(A13);
then f is finite-support by A5, A8, PRE_POLY:def 8;
then reconsider c2 = f as Element of Bags o2 by A11, PRE_POLY:def 12;
take c2 ; :: thesis: c = c1 +^ c2

now :: thesis: for i being object st i in o1 +^ o2 holds
c . i = (c1 +^ c2) . i

let i be object ; :: thesis: ( i in o1 +^ o2 implies c . b₁ = (c1 +^ c2) . b₁ )
assume A14: i in o1 +^ o2 ; :: thesis: c . b₁ = (c1 +^ c2) . b₁

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

suppose A15: i in o1 ; :: thesis: c . b₁ = (c1 +^ c2) . b₁

then reconsider i9 = i as Ordinal ;
dom c1 = o1 by PARTFUN1:def 2;
then c . i9 = c1 . i9 by A15, FUNCT_1:47
.= (c1 +^ c2) . i9 by A15, Def1 ;
hence c . i = (c1 +^ c2) . i ; :: thesis: verum

end;

suppose A16: i in (o1 +^ o2) \ o1 ; :: thesis: c . b₁ = (c1 +^ c2) . b₁

then reconsider i9 = i as Ordinal ;
A17: i9 -^ o1 in o2 by A2, A16, ORDINAL3:60;
not i9 in o1 by A16, XBOOLE_0:def 5;
then o1 c= i9 by ORDINAL1:16;
then c . i9 = c . (o1 +^ (i9 -^ o1)) by ORDINAL3:def 5
.= c2 . (i9 -^ o1) by A7, A17
.= (c1 +^ c2) . i9 by A16, Def1 ;
hence c . i = (c1 +^ c2) . i ; :: thesis: verum

end;

end;

end;

hence c = c1 +^ c2 by PBOOLE:3; :: thesis: verum

end;

end;