let x be set ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being set st [x,y1] in g * f & [x,y2] in g * f holds
y1 = y2
let y1, y2 be set ; :: thesis: ( [x,y1] in g * f & [x,y2] in g * f implies y1 = y2 )
assume [x,y1] in g * f ; :: thesis: ( not [x,y2] in g * f or y1 = y2 )
then consider z1 being set such that
A1: ( [x,z1] in f & [z1,y1] in g ) by RELAT_1:def 8;
assume [x,y2] in g * f ; :: thesis: y1 = y2
then consider z2 being set such that
A2: ( [x,z2] in f & [z2,y2] in g ) by RELAT_1:def 8;
z1 = z2 by A1, A2, Def1;
hence y1 = y2 by A1, A2, Def1; :: thesis: verum