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

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 )
;

end;

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;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

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

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_{1}( Element of o1 +^ o29) -> set = $1 -^ o1;

defpred S_{1}[ 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_{1}(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_{1}(o9) where o9 is Element of o1 +^ o29 : o9 in support c }

ex j being object st S_{1}[i,j]

A7: for i being object st i in o2 holds

S_{1}[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 ) }

{ H_{1}(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

end;A3: support (c | o1) c= support c

proof

dom c = o1 +^ o2
by PARTFUN1:def 2;
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;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

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

defpred S

$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

A5: { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } c= { H

proof

A6:
for i being object st i in o2 holds
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_{1}(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_{1}(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_{1}(o9) where o9 is Element of o1 +^ o29 : o9 in support c }
; :: thesis: verum

end;assume x in { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) } ; :: thesis: x in { H

then ex o9 being Element of o1 +^ o29 st

( x = o9 -^ o1 & o1 c= o9 & o9 in support c ) ;

hence x in { H

ex j being object st S

proof

consider f being ManySortedSet of o2 such that
let i be object ; :: thesis: ( i in o2 implies ex j being object st S_{1}[i,j] )

assume i in o2 ; :: thesis: ex j being object st S_{1}[i,j]

then reconsider x1 = i as Element of o2 ;

take c . (o1 +^ x1) ; :: thesis: S_{1}[i,c . (o1 +^ x1)]

thus S_{1}[i,c . (o1 +^ x1)]
; :: thesis: verum

end;assume i in o2 ; :: thesis: ex j being object st S

then reconsider x1 = i as Element of o2 ;

take c . (o1 +^ x1) ; :: thesis: S

thus S

A7: for i being object st i in o2 holds

S

A8: support f c= { (o9 -^ o1) where o9 is Element of o1 +^ o29 : ( o1 c= o9 & o9 in support c ) }

proof

A11:
f is natural-valued
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;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

proof

A13:
support c is finite
;
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;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

{ H

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

hence
c = c1 +^ c2
by PBOOLE:3; :: thesis: verumc . i = (c1 +^ c2) . i

let i be object ; :: thesis: ( i in o1 +^ o2 implies c . b_{1} = (c1 +^ c2) . b_{1} )

assume A14: i in o1 +^ o2 ; :: thesis: c . b_{1} = (c1 +^ c2) . b_{1}

end;assume A14: i in o1 +^ o2 ; :: thesis: c . b

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

end;

suppose A15:
i in o1
; :: thesis: c . b_{1} = (c1 +^ c2) . b_{1}

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;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

suppose A16:
i in (o1 +^ o2) \ o1
; :: thesis: c . b_{1} = (c1 +^ c2) . b_{1}

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;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