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 } ;
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;
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 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 ;
( [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 )
;
( ( [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 ( [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 }
;
contradictionconsider 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;
verum end; A14:
now ( [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 }
;
contradictionconsider 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;
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 } ) )
verumproof
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 } )
;
( [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 ( ( 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 } ) )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 } )
;
verum
end; end;
now for x, y1, y2 being object st [x,y1] in M & [x,y2] in M holds
y1 = y2let x,
y1,
y2 be
object ;
( [x,y1] in M & [x,y2] in M implies y1 = y2 )assume A22:
(
[x,y1] in M &
[x,y2] in M )
;
y1 = y2hence
y1 = y2
;
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
; 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 ) )
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; verum