let m, n be Function; :: thesis: ( dom m = dom F & ( for x being set st x in dom F holds
m . x = (F . x) . (f . x) ) & dom n = dom F & ( for x being set st x in dom F holds
n . x = (F . x) . (f . x) ) implies m = n )
assume that
A3: dom m = dom F and
A4: for x being set st x in dom F holds
m . x = (F . x) . (f . x) and
A5: dom n = dom F and
A6: for x being set st x in dom F holds
n . x = (F . x) . (f . x) ; :: thesis: m = n
for x being set st x in dom m holds
m . x = n . x

proof

let x be set ; :: thesis: ( x in dom m implies m . x = n . x )
consider g being set such that
A7: g = F . x ;
reconsider g = g as Function by A7;
assume A8: x in dom m ; :: thesis: m . x = n . x
then m . x = g . (f . x) by A3, A4, A7;
hence m . x = n . x by A3, A6, A8, A7; :: thesis: verum

end;

hence m = n by A3, A5, FUNCT_1:2; :: thesis: verum