let x be object ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being object st [x,y1] in g * f & [x,y2] in g * f holds
y1 = y2
let y1, y2 be object ; :: 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 object such that
A1: [x,z1] in f and
A2: [z1,y1] in g by RELAT_1:def 8;
assume [x,y2] in g * f ; :: thesis: y1 = y2
then consider z2 being object such that
A3: [x,z2] in f and
A4: [z2,y2] in g by RELAT_1:def 8;
z1 = z2 by A1, A3, Def1;
hence y1 = y2 by A2, A4, Def1; :: thesis: verum