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 Function-like
proof
let x,
y1,
y2 be
object ;
FUNCT_1:def 1 ( 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] }
;
( 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 A2:
[x,y1] = [o1,F2(o1)]
and
P1[
o1]
;
A3:
o1 = x
by A2, XTUPLE_0:1;
assume
[x,y2] in { [o,F2(o)] where o is Element of F1() : P1[o] }
;
y1 = y2
then consider o2 being
Element of
F1()
such that A4:
[x,y2] = [o2,F2(o2)]
and
P1[
o2]
;
o2 = x
by A4, XTUPLE_0:1;
hence
y1 = y2
by A2, A4, A3, XTUPLE_0:1;
verum
end;
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Relation-like
proof
let x be
object ;
RELAT_1:def 1 ( not x in { [o,F2(o)] where o is Element of F1() : P1[o] } or ex b1, b2 being object st x = [b1,b2] )
assume
x in { [o,F2(o)] where o is Element of F1() : P1[o] }
;
ex b1, b2 being object st x = [b1,b2]
then consider o being
Element of
F1()
such that A5:
x = [o,F2(o)]
and
P1[
o]
;
take
o
;
ex b1 being object st x = [o,b1]
take
F2(
o)
;
x = [o,F2(o)]
thus
x = [o,F2(o)]
by A5;
verum
end;
hence
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Function
by A1; verum