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

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

hence
m = n
by A3, A5; :: thesis: verum
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;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