let F, G be Function; :: thesis: for y being set st y in rng (G * F) & G is one-to-one holds

ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} )

let y be set ; :: thesis: ( y in rng (G * F) & G is one-to-one implies ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} ) )

assume that

A1: y in rng (G * F) and

A2: G is one-to-one ; :: thesis: ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} )

consider x being object such that

A3: x in dom (G * F) and

A4: (G * F) . x = y by A1, FUNCT_1:def 3;

A5: F . x in dom G by A3, FUNCT_1:11;

A6: G . (F . x) = y by A3, A4, FUNCT_1:12;

then G . (F . x) in {y} by TARSKI:def 1;

then A7: F . x in G " {y} by A5, FUNCT_1:def 7;

A8: F " {(F . x)} c= (G * F) " {y}

then consider Fx being object such that

A13: G " {y} = {Fx} by A2, FUNCT_1:74;

x in dom F by A3, FUNCT_1:11;

then A14: F . x in rng F by FUNCT_1:def 3;

A15: F . x in dom G by A3, FUNCT_1:11;

(G * F) " {y} c= F " {(F . x)}

G " {y} = {(F . x)} by A13, A7, TARSKI:def 1;

hence ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} ) by A15, A14, A21; :: thesis: verum

ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} )

let y be set ; :: thesis: ( y in rng (G * F) & G is one-to-one implies ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} ) )

assume that

A1: y in rng (G * F) and

A2: G is one-to-one ; :: thesis: ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} )

consider x being object such that

A3: x in dom (G * F) and

A4: (G * F) . x = y by A1, FUNCT_1:def 3;

A5: F . x in dom G by A3, FUNCT_1:11;

A6: G . (F . x) = y by A3, A4, FUNCT_1:12;

then G . (F . x) in {y} by TARSKI:def 1;

then A7: F . x in G " {y} by A5, FUNCT_1:def 7;

A8: F " {(F . x)} c= (G * F) " {y}

proof

y in rng G
by A1, FUNCT_1:14;
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in F " {(F . x)} or d in (G * F) " {y} )

assume A9: d in F " {(F . x)} ; :: thesis: d in (G * F) " {y}

A10: d in dom F by A9, FUNCT_1:def 7;

F . d in {(F . x)} by A9, FUNCT_1:def 7;

then A11: F . d = F . x by TARSKI:def 1;

then G . (F . d) in {y} by A6, TARSKI:def 1;

then A12: (G * F) . d in {y} by A10, FUNCT_1:13;

d in dom (G * F) by A5, A10, A11, FUNCT_1:11;

hence d in (G * F) " {y} by A12, FUNCT_1:def 7; :: thesis: verum

end;assume A9: d in F " {(F . x)} ; :: thesis: d in (G * F) " {y}

A10: d in dom F by A9, FUNCT_1:def 7;

F . d in {(F . x)} by A9, FUNCT_1:def 7;

then A11: F . d = F . x by TARSKI:def 1;

then G . (F . d) in {y} by A6, TARSKI:def 1;

then A12: (G * F) . d in {y} by A10, FUNCT_1:13;

d in dom (G * F) by A5, A10, A11, FUNCT_1:11;

hence d in (G * F) " {y} by A12, FUNCT_1:def 7; :: thesis: verum

then consider Fx being object such that

A13: G " {y} = {Fx} by A2, FUNCT_1:74;

x in dom F by A3, FUNCT_1:11;

then A14: F . x in rng F by FUNCT_1:def 3;

A15: F . x in dom G by A3, FUNCT_1:11;

(G * F) " {y} c= F " {(F . x)}

proof

then A21:
F " {(F . x)} = (G * F) " {y}
by A8;
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in (G * F) " {y} or d in F " {(F . x)} )

assume A16: d in (G * F) " {y} ; :: thesis: d in F " {(F . x)}

A17: d in dom (G * F) by A16, FUNCT_1:def 7;

then A18: d in dom F by FUNCT_1:11;

(G * F) . d in {y} by A16, FUNCT_1:def 7;

then A19: G . (F . d) in {y} by A17, FUNCT_1:12;

A20: F . d in dom G by A17, FUNCT_1:11;

F . x = Fx by A13, A7, TARSKI:def 1;

then F . d in {(F . x)} by A13, A20, A19, FUNCT_1:def 7;

hence d in F " {(F . x)} by A18, FUNCT_1:def 7; :: thesis: verum

end;assume A16: d in (G * F) " {y} ; :: thesis: d in F " {(F . x)}

A17: d in dom (G * F) by A16, FUNCT_1:def 7;

then A18: d in dom F by FUNCT_1:11;

(G * F) . d in {y} by A16, FUNCT_1:def 7;

then A19: G . (F . d) in {y} by A17, FUNCT_1:12;

A20: F . d in dom G by A17, FUNCT_1:11;

F . x = Fx by A13, A7, TARSKI:def 1;

then F . d in {(F . x)} by A13, A20, A19, FUNCT_1:def 7;

hence d in F " {(F . x)} by A18, FUNCT_1:def 7; :: thesis: verum

G " {y} = {(F . x)} by A13, A7, TARSKI:def 1;

hence ex x being set st

( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} ) by A15, A14, A21; :: thesis: verum