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}

proof

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;

y in rng G by A1, FUNCT_1:14;
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

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;

then A21: F " {(F . x)} = (G * F) " {y} by A8;
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