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 ;
A5: F . x in dom G by ;
A6: G . (F . x) = y by ;
then G . (F . x) in {y} by TARSKI:def 1;
then A7: F . x in G " {y} by ;
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 ;
F . d in {(F . x)} by ;
then A11: F . d = F . x by TARSKI:def 1;
then G . (F . d) in {y} by ;
then A12: (G * F) . d in {y} by ;
d in dom (G * F) by ;
hence d in (G * F) " {y} by ; :: thesis: verum
end;
y in rng G by ;
then consider Fx being object such that
A13: G " {y} = {Fx} by ;
x in dom F by ;
then A14: F . x in rng F by FUNCT_1:def 3;
A15: F . x in dom G by ;
(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 ;
then A18: d in dom F by FUNCT_1:11;
(G * F) . d in {y} by ;
then A19: G . (F . d) in {y} by ;
A20: F . d in dom G by ;
F . x = Fx by ;
then F . d in {(F . x)} by ;
hence d in F " {(F . x)} by ; :: thesis: verum
end;
then A21: F " {(F . x)} = (G * F) " {y} by A8;
G " {y} = {(F . x)} by ;
hence ex x being set st
( x in dom G & x in rng F & G " {y} = {x} & F " {x} = (G * F) " {y} ) by ; :: thesis: verum