set M1 = { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ;
set M2 = { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ;
set M = { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } \/ { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ;

now

let u be set ; :: thesis: ( u in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } \/ { [b',(0. L)] where b' is Element of Bags n : not b divides b' } implies u in [:(Bags n),the carrier of L:] )
assume A1: u in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } \/ { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ; :: thesis: u in [:(Bags n),the carrier of L:]

now

per cases ( u in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } or u in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) by A1, XBOOLE_0:def 3;

case u in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ; :: thesis: u in [:(Bags n),the carrier of L:]

then ex b' being Element of Bags n st
( u = [b',(p . (b' -' b))] & b divides b' ) ;
hence u in [:(Bags n),the carrier of L:] by ZFMISC_1:def 2; :: thesis: verum

end;

case u in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ; :: thesis: u in [:(Bags n),the carrier of L:]

then ex b' being Element of Bags n st
( u = [b',(0. L)] & not b divides b' ) ;
hence u in [:(Bags n),the carrier of L:] by ZFMISC_1:def 2; :: thesis: verum

end;

end;

end;

hence u in [:(Bags n),the carrier of L:] ; :: thesis: verum

end;

then reconsider M = { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } \/ { [b',(0. L)] where b' is Element of Bags n : not b divides b' } as Relation of , by TARSKI:def 3;

A2: now

let u be set ; :: thesis: ( u in Bags n implies u in dom M )
assume u in Bags n ; :: thesis: u in dom M
then reconsider u' = u as bag of n by PRE_POLY:def 12;
A3: u' is Element of Bags n by PRE_POLY:def 12;

now

per cases ( not b divides u' or b divides u' ) ;

case not b divides u' ; :: thesis: u in dom M

then [u',(0. L)] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } by A3;
then [u',(0. L)] in M by XBOOLE_0:def 3;
hence u in dom M by RELAT_1:def 4; :: thesis: verum

end;

case b divides u' ; :: thesis: u in dom M

then [u',(p . (u' -' b))] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } by A3;
then [u',(p . (u' -' b))] in M by XBOOLE_0:def 3;
hence u in dom M by RELAT_1:def 4; :: thesis: verum

end;

end;

end;

hence u in dom M ; :: thesis: verum

end;

for u being set st u in dom M holds
u in Bags n ;
then A4: dom M = Bags n by A2, TARSKI:2;

A5: now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in M & [x,y2] in M & not ( [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } & [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) implies ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) )
assume A6: ( [x,y1] in M & [x,y2] in M ) ; :: thesis: ( ( [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } & [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) or ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) )

A7: now

assume that
A8: [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } and
A9: [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ; :: thesis: contradiction
consider v being Element of Bags n such that
A10: [v,(0. L)] = [x,y1] and
A11: not b divides v by A8;
consider u being Element of Bags n such that
A12: [u,(p . (u -' b))] = [x,y2] and
A13: b divides u by A9;
u = [x,y2] `1 by A12, MCART_1:def 1
.= x by MCART_1:def 1
.= [v,(0. L)] `1 by A10, MCART_1:def 1
.= v by MCART_1:def 1 ;
hence contradiction by A13, A11; :: thesis: verum

end;

A14: now

assume that
A15: [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } and
A16: [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ; :: thesis: contradiction
consider v being Element of Bags n such that
A17: [v,(0. L)] = [x,y2] and
A18: not b divides v by A16;
consider u being Element of Bags n such that
A19: [u,(p . (u -' b))] = [x,y1] and
A20: b divides u by A15;
u = [x,y1] `1 by A19, MCART_1:def 1
.= x by MCART_1:def 1
.= [v,(0. L)] `1 by A17, MCART_1:def 1
.= v by MCART_1:def 1 ;
hence contradiction by A20, A18; :: thesis: verum

end;

thus ( ( [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } & [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) or ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) ) :: thesis: verum

proof

assume A21: ( not [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } or not [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) ; :: thesis: ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } )

now

per cases ( not [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } or not [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) by A21;

case not [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ; :: thesis: ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } )

hence ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) by A6, A7, XBOOLE_0:def 3; :: thesis: verum

end;

case not [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ; :: thesis: ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } )

hence ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) by A6, A14, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) ; :: thesis: verum

end;

end;

now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in M & [x,y2] in M implies y1 = y2 )
assume A22: ( [x,y1] in M & [x,y2] in M ) ; :: thesis: y1 = y2

now

per cases ( ( [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } & [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) or ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) ) by A5, A22;

case A23: ( [x,y1] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } & [x,y2] in { [b',(p . (b' -' b))] where b' is Element of Bags n : b divides b' } ) ; :: thesis: y1 = y2

then consider v being Element of Bags n such that
A24: [v,(p . (v -' b))] = [x,y2] and
b divides v ;
consider u being Element of Bags n such that
A25: [u,(p . (u -' b))] = [x,y1] and
b divides u by A23;
u = [x,y1] `1 by A25, MCART_1:def 1
.= x by MCART_1:def 1
.= [v,(p . (v -' b))] `1 by A24, MCART_1:def 1
.= v by MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A25, A24, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

case A26: ( [x,y1] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } & [x,y2] in { [b',(0. L)] where b' is Element of Bags n : not b divides b' } ) ; :: thesis: y1 = y2

then A27: ex v being Element of Bags n st
( [v,(0. L)] = [x,y2] & not b divides v ) ;
A28: ex u being Element of Bags n st
( [u,(0. L)] = [x,y1] & not b divides u ) by A26;
thus y1 = [x,y1] `2 by MCART_1:def 2
.= 0. L by A28, MCART_1:def 2
.= [x,y2] `2 by A27, MCART_1:def 2
.= y2 by MCART_1:def 2 ; :: thesis: verum

end;

end;

end;

hence y1 = y2 ; :: thesis: verum

end;

then reconsider M = M as Function of Bags n,the carrier of L by A4, FUNCT_1:def 1, FUNCT_2:def 1;
reconsider M = M as Function of Bags n,L ;
take M ; :: thesis: for b' being bag of n st b divides b' holds
( M . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
M . b' = 0. L ) )

A29: now

let b' be bag of n; :: thesis: ( not b divides b' implies M . b' = 0. L )
A30: b' is Element of Bags n by PRE_POLY:def 12;
assume not b divides b' ; :: thesis: M . b' = 0. L
then [b',(0. L)] in { [u,(0. L)] where u is Element of Bags n : not b divides u } by A30;
then [b',(0. L)] in M by XBOOLE_0:def 3;
hence M . b' = 0. L by FUNCT_1:8; :: thesis: verum

end;

now

let b' be bag of n; :: thesis: ( b divides b' implies M . b' = p . (b' -' b) )
A31: b' is Element of Bags n by PRE_POLY:def 12;
assume b divides b' ; :: thesis: M . b' = p . (b' -' b)
then [b',(p . (b' -' b))] in { [u,(p . (u -' b))] where u is Element of Bags n : b divides u } by A31;
then [b',(p . (b' -' b))] in M by XBOOLE_0:def 3;
hence M . b' = p . (b' -' b) by FUNCT_1:8; :: thesis: verum

end;

hence for b' being bag of n st b divides b' holds
( M . b' = p . (b' -' b) & ( for b' being bag of n st not b divides b' holds
M . b' = 0. L ) ) by A29; :: thesis: verum