let IT1, IT2 be Function; :: thesis: ( dom IT1 = dom f & ( for x being set st x in dom f holds

IT1 . x = g * (f . x) ) & dom IT2 = dom f & ( for x being set st x in dom f holds

IT2 . x = g * (f . x) ) implies IT1 = IT2 )

assume A2: ( dom IT1 = dom f & ( for x being set st x in dom f holds

IT1 . x = g * (f . x) ) ) ; :: thesis: ( not dom IT2 = dom f or ex x being set st

( x in dom f & not IT2 . x = g * (f . x) ) or IT1 = IT2 )

assume A3: ( dom IT2 = dom f & ( for x being set st x in dom f holds

IT2 . x = g * (f . x) ) ) ; :: thesis: IT1 = IT2

IT1 . x = g * (f . x) ) & dom IT2 = dom f & ( for x being set st x in dom f holds

IT2 . x = g * (f . x) ) implies IT1 = IT2 )

assume A2: ( dom IT1 = dom f & ( for x being set st x in dom f holds

IT1 . x = g * (f . x) ) ) ; :: thesis: ( not dom IT2 = dom f or ex x being set st

( x in dom f & not IT2 . x = g * (f . x) ) or IT1 = IT2 )

assume A3: ( dom IT2 = dom f & ( for x being set st x in dom f holds

IT2 . x = g * (f . x) ) ) ; :: thesis: IT1 = IT2

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

IT1 . x = IT2 . x

hence
IT1 = IT2
by A2, A3, FUNCT_1:2; :: thesis: verumIT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )

assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x

then ( IT1 . x = g * (f . x) & IT2 . x = g * (f . x) ) by A2, A3;

hence IT1 . x = IT2 . x ; :: thesis: verum

end;assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x

then ( IT1 . x = g * (f . x) & IT2 . x = g * (f . x) ) by A2, A3;

hence IT1 . x = IT2 . x ; :: thesis: verum