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 :: thesis: for u being object st 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 } holds
u in [:(Bags n), the carrier of L:]
let u be object ; :: 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 :: thesis: ( ( u in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } & u in [:(Bags n), the carrier of L:] ) or ( u in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } & u in [:(Bags n), the carrier of L:] ) )
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 :: thesis: for u being object st u in Bags n holds
u in dom M
let u be object ; :: 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 :: thesis: ( ( not b divides u9 & u in dom M ) or ( b divides u9 & u in dom M ) )
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 XTUPLE_0:def 12; :: 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 XTUPLE_0:def 12; :: thesis: verum
end;
end;
end;
hence u in dom M ; :: thesis: verum
end;
for u being object st u in dom M holds
u in Bags n ;
then A4: dom M = Bags n by A2, TARSKI:2;
A5: now :: thesis: for x, y1, y2 being object st [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 } ) holds
( [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 } )
let x, y1, y2 be object ; :: 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 :: thesis: ( [x,y1] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } implies not [x,y2] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } )
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 by A12, XTUPLE_0:1
.= v by A10, XTUPLE_0:1 ;
hence contradiction by A13, A11; :: thesis: verum
end;
A14: now :: thesis: ( [x,y1] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } implies not [x,y2] in { [b9,(0. L)] where b9 is Element of Bags n : not b divides b9 } )
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 by A19, XTUPLE_0:1
.= v by A17, XTUPLE_0: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 :: thesis: ( ( not [x,y1] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } & [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 } ) or ( not [x,y2] in { [b9,(p . (b9 -' b))] where b9 is Element of Bags n : b divides b9 } & [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 } ) )
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 :: thesis: for x, y1, y2 being object st [x,y1] in M & [x,y2] in M holds
y1 = y2
let x, y1, y2 be object ; :: 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 :: 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 } & y1 = y2 ) 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 } & y1 = y2 ) )
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 by A25, XTUPLE_0:1
.= v by A24, XTUPLE_0:1 ;
hence y1 = p . (v -' b) by A25, XTUPLE_0:1
.= y2 by A24, XTUPLE_0:1 ;
:: 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 = 0. L by A28, XTUPLE_0:1
.= y2 by A27, XTUPLE_0:1 ; :: 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 :: thesis: for b9 being bag of n st not b divides b9 holds
M . b9 = 0. L
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 :: thesis: for b9 being bag of n st b divides b9 holds
M . b9 = p . (b9 -' b)
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