let F be Function; :: thesis: ex X being set st
( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )
defpred S1[ object , object ] means F . $2 = $1;
A1: for x being object st x in rng F holds
ex y being object st
( y in dom F & S1[x,y] ) by FUNCT_1:def 3;
consider g being Function of (rng F),(dom F) such that
A2: for x being object st x in rng F holds
S1[x,g . x] from FUNCT_2:sch 1(A1);
 take X = rng g; :: thesis: ( X c= dom F & rng F = rng (F | X) & F | X is one-to-one )
set FX = F | X;
( dom F = {} iff rng F = {} ) by RELAT_1:42;
then A3: dom g = rng F by FUNCT_2:def 1;
thus A4: X c= dom F by RELAT_1:def 19; :: thesis: ( rng F = rng (F | X) & F | X is one-to-one )
A5: rng F c= rng (F | X)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in rng (F | X) )
assume y in rng F ; :: thesis: y in rng (F | X)
then ( g . y in X & F . (g . y) = y ) by A2, A3, FUNCT_1:def 3;
hence y in rng (F | X) by A4, FUNCT_1:50; :: thesis: verum
end;
rng (F | X) c= rng F by RELAT_1:70;
hence rng F = rng (F | X) by A5; :: thesis: F | X is one-to-one
now :: thesis: for x1, x2 being object st x1 in dom (F | X) & x2 in dom (F | X) & (F | X) . x1 = (F | X) . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom (F | X) & x2 in dom (F | X) & (F | X) . x1 = (F | X) . x2 implies x1 = x2 )
assume that
A6: x1 in dom (F | X) and
A7: x2 in dom (F | X) and
A8: (F | X) . x1 = (F | X) . x2 ; :: thesis: x1 = x2
A9: ( (F | X) . x1 = F . x1 & (F | X) . x2 = F . x2 ) by A6, A7, FUNCT_1:47;
A10: dom (F | X) c= X by RELAT_1:58;
then consider y1 being object such that
A11: y1 in dom g and
A12: g . y1 = x1 by A6, FUNCT_1:def 3;
consider y2 being object such that
A13: ( y2 in dom g & g . y2 = x2 ) by A7, A10, FUNCT_1:def 3;
F . x1 = y1 by A2, A3, A11, A12;
hence x1 = x2 by A2, A3, A8, A9, A12, A13; :: thesis: verum
end;
hence F | X is one-to-one by FUNCT_1:def 4; :: thesis: verum