deffunc H1( set ) -> set = pr1 (F . $1);
consider X being ManySortedSet of such that
A1:
for i being set st i in I holds
X . i = H1(i)
from PBOOLE:sch 4();
X is ManySortedFunction of A,B
proof
let i be
set ;
:: according to PBOOLE:def 18 :: thesis: ( not i in I or X . i is Element of bool [:(A . i),(B . i):] )
assume A2:
i in I
;
:: thesis: X . i is Element of bool [:(A . i),(B . i):]
then A3:
[|B,C|] . i <> {}
;
A4:
X . i = pr1 (F . i)
by A1, A2;
reconsider Bi =
B . i as non
empty set by A2;
reconsider Xi =
X . i as
Function by A4;
A5:
F . i is
Function of
(A . i),
([|B,C|] . i)
by A2, PBOOLE:def 18;
then
dom (F . i) = A . i
by A3, FUNCT_2:def 1;
then A6:
dom Xi = A . i
by A4, MCART_1:def 12;
rng Xi c= Bi
proof
let q be
set ;
:: according to TARSKI:def 3 :: thesis: ( not q in rng Xi or q in Bi )
assume A7:
q in rng Xi
;
:: thesis: q in Bi
assume A8:
not
q in Bi
;
:: thesis: contradiction
consider x being
set such that A9:
x in dom Xi
and A10:
Xi . x = q
by A7, FUNCT_1:def 5;
A11:
x in dom (F . i)
by A4, A9, MCART_1:def 12;
then A12:
Xi . x = ((F . i) . x) `1
by A4, MCART_1:def 12;
rng (F . i) c= [|B,C|] . i
by A5, RELAT_1:def 19;
then A13:
rng (F . i) c= [:(B . i),(C . i):]
by A2, PBOOLE:def 21;
(F . i) . x in rng (F . i)
by A11, FUNCT_1:def 5;
hence
contradiction
by A8, A10, A12, A13, MCART_1:10;
:: thesis: verum
end;
hence
X . i is
Element of
bool [:(A . i),(B . i):]
by A6, FUNCT_2:def 1, RELSET_1:11;
:: thesis: verum
end;
then reconsider X = X as ManySortedFunction of A,B ;
take
X
; :: thesis: for i being set st i in I holds
X . i = pr1 (F . i)
thus
for i being set st i in I holds
X . i = pr1 (F . i)
by A1; :: thesis: verum