set f = { [o,F2(o)] where o is Element of F1() : P1[o] } ;
A1:
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Relation-like
proof
let x be
set ;
:: according to RELAT_1:def 1 :: thesis: ( not x in { [o,F2(o)] where o is Element of F1() : P1[o] } or ex b1, b2 being set st x = [b1,b2] )
assume
x in { [o,F2(o)] where o is Element of F1() : P1[o] }
;
:: thesis: ex b1, b2 being set st x = [b1,b2]
then consider o being
Element of
F1()
such that A2:
x = [o,F2(o)]
and
P1[
o]
;
take
o
;
:: thesis: ex b1 being set st x = [o,b1]
take
F2(
o)
;
:: thesis: x = [o,F2(o)]
thus
x = [o,F2(o)]
by A2;
:: thesis: verum
end;
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Function-like
proof
let x,
y1,
y2 be
set ;
:: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in { [o,F2(o)] where o is Element of F1() : P1[o] } or not [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } or y1 = y2 )
assume
[x,y1] in { [o,F2(o)] where o is Element of F1() : P1[o] }
;
:: thesis: ( not [x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] } or y1 = y2 )
then consider o1 being
Element of
F1()
such that A3:
[x,y1] = [o1,F2(o1)]
and
P1[
o1]
;
assume
[x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] }
;
:: thesis: y1 = y2
then consider o2 being
Element of
F1()
such that A4:
[x,y2] = [o2,F2(o2)]
and
P1[
o2]
;
(
o1 = x &
o2 = x )
by A3, A4, ZFMISC_1:33;
hence
y1 = y2
by A3, A4, ZFMISC_1:33;
:: thesis: verum
end;
hence
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Function
by A1; :: thesis: verum