let x, z be object ; :: thesis: for f, g being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )
let f, g be Function; :: thesis: ( [x,z] in g * f implies ( [x,(f . x)] in f & [(f . x),z] in g ) )
assume [x,z] in g * f ; :: thesis: ( [x,(f . x)] in f & [(f . x),z] in g )
then ex y being object st
( [x,y] in f & [y,z] in g ) by RELAT_1:def 8;
hence ( [x,(f . x)] in f & [(f . x),z] in g ) by FUNCT_1:1; :: thesis: verum