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 set such that
A3: ( x in dom (G * F) & (G * F) . x = y ) by A1, FUNCT_1:def 5;
A4: ( F . x in dom G & G . (F . x) = y ) by A3, FUNCT_1:21, FUNCT_1:22;
y in rng G by A1, FUNCT_1:25;
then consider Fx being set such that
A5: G " {y} = {Fx} by A2, FUNCT_1:144;
( G . (F . x) in {y} & F . x in dom G ) by A4, TARSKI:def 1;
then A6: F . x in G " {y} by FUNCT_1:def 13;
A7: F " {(F . x)} c= (G * F) " {y}

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in F " {(F . x)} or d in (G * F) " {y} )
assume A8: d in F " {(F . x)} ; :: thesis: d in (G * F) " {y}
F . d in {(F . x)} by A8, FUNCT_1:def 13;
then ( d in dom F & F . d = F . x ) by A8, FUNCT_1:def 13, TARSKI:def 1;
then ( d in dom F & d in dom (G * F) & G . (F . d) in {y} ) by A4, FUNCT_1:21, TARSKI:def 1;
then ( d in dom (G * F) & (G * F) . d in {y} ) by FUNCT_1:23;
hence d in (G * F) " {y} by FUNCT_1:def 13; :: thesis: verum

end;

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

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in (G * F) " {y} or d in F " {(F . x)} )
assume A9: d in (G * F) " {y} ; :: thesis: d in F " {(F . x)}
( d in dom (G * F) & (G * F) . d in {y} ) by A9, FUNCT_1:def 13;
then A10: ( d in dom F & F . d in dom G & G . (F . d) in {y} & F . x = Fx ) by A5, A6, FUNCT_1:21, FUNCT_1:22, TARSKI:def 1;
then F . d in {(F . x)} by A5, FUNCT_1:def 13;
hence d in F " {(F . x)} by A10, FUNCT_1:def 13; :: thesis: verum

end;

then ( x in dom F & F " {(F . x)} = (G * F) " {y} ) by A3, A7, FUNCT_1:21, XBOOLE_0:def 10;
then ( F . x in dom G & F . x in rng F & G " {y} = {(F . x)} & F " {(F . x)} = (G * F) " {y} ) by A3, A5, A6, FUNCT_1:21, FUNCT_1:def 5, 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} ) ; :: thesis: verum