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

proof

let x be object ; :: 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 A9: m . x = g . (f . x) by A4, A7;
x in dom n by A3, A5, A8;
hence m . x = n . x by A6, A7, A9; :: thesis: verum

end;

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