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

now

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

now

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

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

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

end;

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

then ex b9 being Element of Bags n st
( u = [b9,(0. L)] & not b divides b9 ) ;
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 = { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } \/ { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } as Relation of (Bags n), the carrier of L 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 u9 = u as bag of n ;
A3: u9 is Element of Bags n by PRE_POLY:def 12;

now

per cases ( not b divides u9 or b divides u9 ) ;

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

then [u9,(0. L)] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } by A3;
then [u9,(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 u9 ; :: thesis: u in dom M

then [u9,(p . (u9 -' b))] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } by A3;
then [u9,(p . (u9 -' 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:1;

A5: now

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

A7: now

assume that
A8: [x,y1] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } and
A9: [x,y2] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } ; :: 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 { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } and
A16: [x,y2] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } ; :: 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 { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } & [x,y2] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } ) or ( [x,y1] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } & [x,y2] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } ) ) :: thesis: verum

proof

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

now

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

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

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

end;

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

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

end;

end;

end;

hence ( [x,y1] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } & [x,y2] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } ) ; :: 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 { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } & [x,y2] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } ) or ( [x,y1] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } & [x,y2] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } ) ) by A5, A22;

case A23: ( [x,y1] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } & [x,y2] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } ) ; :: 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 { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } & [x,y2] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } ) ; :: 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 b9 being bag of n st b divides b9 holds
( M . b9 = p . (b9 -' b) & ( for b9 being bag of n st not b divides b9 holds
M . b9 = 0. L ) )

A29: now

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

end;

now

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

end;

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