set f = { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } ;

A1: { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } is Function-like
_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } is Relation-like
_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } is Function
by A1; :: thesis: verum

A1: { [o,F

proof

{ [o,F
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } or not [x,y2] in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } or y1 = y2 )

assume [x,y1] in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] }
; :: thesis: ( not [x,y2] in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } or y1 = y2 )

then consider o1 being Element of F_{1}() such that

A2: [x,y1] = [o1,F_{2}(o1)]
and

P_{1}[o1]
;

A3: o1 = x by A2, XTUPLE_0:1;

assume [x,y2] in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] }
; :: thesis: y1 = y2

then consider o2 being Element of F_{1}() such that

A4: [x,y2] = [o2,F_{2}(o2)]
and

P_{1}[o2]
;

o2 = x by A4, XTUPLE_0:1;

hence y1 = y2 by A2, A4, A3, XTUPLE_0:1; :: thesis: verum

end;assume [x,y1] in { [o,F

then consider o1 being Element of F

A2: [x,y1] = [o1,F

P

A3: o1 = x by A2, XTUPLE_0:1;

assume [x,y2] in { [o,F

then consider o2 being Element of F

A4: [x,y2] = [o2,F

P

o2 = x by A4, XTUPLE_0:1;

hence y1 = y2 by A2, A4, A3, XTUPLE_0:1; :: thesis: verum

proof

hence
{ [o,F
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] } or ex b_{1}, b_{2} being object st x = [b_{1},b_{2}] )

assume x in { [o,F_{2}(o)] where o is Element of F_{1}() : P_{1}[o] }
; :: thesis: ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]

then consider o being Element of F_{1}() such that

A5: x = [o,F_{2}(o)]
and

P_{1}[o]
;

take o ; :: thesis: ex b_{1} being object st x = [o,b_{1}]

take F_{2}(o)
; :: thesis: x = [o,F_{2}(o)]

thus x = [o,F_{2}(o)]
by A5; :: thesis: verum

end;assume x in { [o,F

then consider o being Element of F

A5: x = [o,F

P

take o ; :: thesis: ex b

take F

thus x = [o,F