let x, z be set ; :: thesis: for g, f being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )
let g, f 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 set 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:8; :: thesis: verum