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 & ( for x being set st x in dom F holds
m . x = (F . x) . (f . x) ) ) and
A4: ( dom n = dom F & ( 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 )
assume A5: x in dom m ; :: thesis: m . x = n . x
consider g being set such that
A6: g = F . x ;
reconsider g = g as Function by A6;
( m . x = g . (f . x) & n . x = g . (f . x) ) by A3, A4, A5, A6;
hence m . x = n . x ; :: thesis: verum

end;

hence m = n by A3, A4, FUNCT_1:9; :: thesis: verum