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 ; :: 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
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] } ; :: thesis: 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; :: thesis: verum
end;
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Relation-like
proof
let x be object ; :: 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 object st x = [b1,b2] )
assume x in { [o,F2(o)] where o is Element of F1() : P1[o] } ; :: thesis: 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 ; :: thesis: ex b1 being object st x = [o,b1]
take F2(o) ; :: thesis: x = [o,F2(o)]
thus x = [o,F2(o)] by A5; :: thesis: verum
end;
hence { [o,F2(o)] where o is Element of F1() : P1[o] } is Function by A1; :: thesis: verum