set A = (dom f) /\ (dom g);
let IT1, IT2 be Function; :: thesis: ( dom IT1 = (dom f) /\ (dom g) & ( for x being set st x in dom IT1 holds
IT1 . x = (f . x) . (g . x) ) & dom IT2 = (dom f) /\ (dom g) & ( for x being set st x in dom IT2 holds
IT2 . x = (f . x) . (g . x) ) implies IT1 = IT2 )
assume A2: ( dom IT1 = (dom f) /\ (dom g) & ( for x being set st x in dom IT1 holds
IT1 . x = (f . x) . (g . x) ) ) ; :: thesis: ( not dom IT2 = (dom f) /\ (dom g) or ex x being set st
( x in dom IT2 & not IT2 . x = (f . x) . (g . x) ) or IT1 = IT2 )
assume A3: ( dom IT2 = (dom f) /\ (dom g) & ( for x being set st x in dom IT2 holds
IT2 . x = (f . x) . (g . x) ) ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object st x in dom IT1 holds
IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume A4: x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
thus IT1 . x = (f . x) . (g . x) by A2, A4
.= IT2 . x by A2, A3, A4 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_1:2, A2, A3; :: thesis: verum