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 c1 = c as Element of Bags o1 by ORDINAL2:44;
take c1 ; :: thesis: ex c2 being Element of Bags o2 st c = c1 +^ c2
reconsider c2 = {} as Element of Bags o2 by A1, POLYNOM1:55, TARSKI:def 1;
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 o2' = o2 as non empty Ordinal ;
support (c | o1) c= support c

proof

let x be set ; :: 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 A3: (c | o1) . x <> 0 by POLYNOM1:def 7;
then x in dom (c | o1) by FUNCT_1:def 4;
then [x,((c | o1) . x)] in c | o1 by FUNCT_1:8;
then [x,((c | o1) . x)] in c by RELAT_1:def 11;
then (c | o1) . x = c . x by FUNCT_1:8;
hence x in support c by A3, POLYNOM1:def 7; :: thesis: verum

end;

then A4: support (c | o1) is finite ;
dom c = o1 +^ o2 by PARTFUN1:def 4;
then o1 c= dom c by ORDINAL3:27;
then dom (c | o1) = o1 by RELAT_1:91;
then c | o1 is bag of by A4, PARTFUN1:def 4, POLYNOM1:def 8, RELAT_1:def 18;
then reconsider c1 = c | o1 as Element of Bags o1 by POLYNOM1:def 14;
take c1 ; :: thesis: ex c2 being Element of Bags o2 st c = c1 +^ c2
defpred S₁[ set , set ] means for x1 being Element of o2 st x1 = $1 holds
$2 = c . (o1 +^ x1);
A5: for i being set st i in o2 holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in o2 implies ex j being set st S₁[i,j] )
assume i in o2 ; :: thesis: ex j being set 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 such that
A6: for i being set st i in o2 holds
S₁[i,f . i] from PBOOLE:sch 3(A5);
A7: 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 A8: x in dom f ; :: thesis: f . x is natural
then A9: x in o2 by PARTFUN1:def 4;
reconsider o = x as Element of o2 by A8, PARTFUN1:def 4;
f . x = c . (o1 +^ o) by A6, A9;
hence f . x is natural ; :: thesis: verum

end;

deffunc H₁( Element of o1 +^ o2') -> set = $1 -^ o1;
set B = { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } ;
set C = { H₁(o') where o' is Element of o1 +^ o2' : o' in support c } ;
A10: support c is finite ;
A11: { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } c= { H₁(o') where o' is Element of o1 +^ o2' : o' in support c }

proof

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

end;

{ H₁(o') where o' is Element of o1 +^ o2' : o' in support c } is finite from FRAENKEL:sch 21(A10);
then A12: { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } is finite by A11;
support f = { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) }

proof

thus support f c= { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } :: according to XBOOLE_0:def 10 :: thesis: { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } c= support f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } )
assume x in support f ; :: thesis: x in { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) }
then A13: f . x <> 0 by POLYNOM1:def 7;
then x in dom f by FUNCT_1:def 4;
then reconsider o' = x as Element of o2' by PARTFUN1:def 4;
c . (o1 +^ o') <> 0 by A6, A13;
then A14: o1 +^ o' in support c by POLYNOM1:def 7;
reconsider o'' = o1 +^ o' as Element of o1 +^ o2' by ORDINAL2:49;
A15: o' = o'' -^ o1 by ORDINAL3:65;
o1 c= o'' by ORDINAL3:27;
hence x in { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } by A14, A15; :: thesis: verum

end;

thus { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } c= support f :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } or x in support f )
assume x in { (o' -^ o1) where o' is Element of o1 +^ o2' : ( o1 c= o' & o' in support c ) } ; :: thesis: x in support f
then consider o' being Element of o1 +^ o2' such that
A16: x = o' -^ o1 and
A17: o1 c= o' and
A18: o' in support c ;
A19: c . o' <> 0 by A18, POLYNOM1:def 7;
o' -^ o1 in (o1 +^ o2') -^ o1 by A17, ORDINAL3:66;
then A20: o' -^ o1 in o2' by ORDINAL3:65;
c . (o1 +^ (o' -^ o1)) <> 0 by A17, A19, ORDINAL3:def 6;
then f . x <> 0 by A6, A16, A20;
hence x in support f by POLYNOM1:def 7; :: thesis: verum

end;

end;

then f is finite-support by A12, POLYNOM1:def 8;
then reconsider c2 = f as Element of Bags o2 by A7, POLYNOM1:def 14;
take c2 ; :: thesis: c = c1 +^ c2

now

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

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

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

then reconsider i' = i as Ordinal ;
dom c1 = o1 by PARTFUN1:def 4;
then c . i' = c1 . i' by A22, FUNCT_1:70
.= (c1 +^ c2) . i' by A22, Def1 ;
hence c . i = (c1 +^ c2) . i ; :: thesis: verum

end;

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

then reconsider i' = i as Ordinal ;
A24: i' -^ o1 in o2 by A2, A23, ORDINAL3:73;
not i' in o1 by A23, XBOOLE_0:def 5;
then o1 c= i' by ORDINAL1:26;
then c . i' = c . (o1 +^ (i' -^ o1)) by ORDINAL3:def 6
.= c2 . (i' -^ o1) by A6, A24
.= (c1 +^ c2) . i' by A23, Def1 ;
hence c . i = (c1 +^ c2) . i ; :: thesis: verum

end;

end;

end;

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

end;

end;