let X, Y be non empty set ; :: thesis: for X0, Y0 being set
for f being Function of X,Y st f is bijective & rng (f | X0) = Y0 holds
(f | X0) " = (f ") | Y0
let X0, Y0 be set ; :: thesis: for f being Function of X,Y st f is bijective & rng (f | X0) = Y0 holds
(f | X0) " = (f ") | Y0
let f be Function of X,Y; :: thesis: ( f is bijective & rng (f | X0) = Y0 implies (f | X0) " = (f ") | Y0 )
assume that
A1: f is bijective and
A2: rng (f | X0) = Y0 ; :: thesis: (f | X0) " = (f ") | Y0
A3: ( rng f = dom (f ") & dom f = rng (f ") ) by A1, FUNCT_1:33;
A4: ( rng f = Y & Y = dom (f ") ) by A1, A3, FUNCT_2:def 3;
A5: dom ((f ") | Y0) = Y0 by A2, A4, RELAT_1:62;
A6: f | X0 is one-to-one by A1, FUNCT_1:52;
then A7: ( rng (f | X0) = dom ((f | X0) ") & dom (f | X0) = rng ((f | X0) ") ) by FUNCT_1:33;
A8: dom ((f | X0) ") = Y0 by A2, A6, FUNCT_1:33;
for x being object st x in dom ((f ") | Y0) holds
((f ") | Y0) . x = ((f | X0) ") . x
proof
let x be object ; :: thesis: ( x in dom ((f ") | Y0) implies ((f ") | Y0) . x = ((f | X0) ") . x )
assume x in dom ((f ") | Y0) ; :: thesis: ((f ") | Y0) . x = ((f | X0) ") . x
then A9: x in Y0 by A2, A4, RELAT_1:62;
then A10: ((f ") | Y0) . x = (f ") . x by FUNCT_1:49;
A11: x in dom ((f | X0) ") by A2, A6, A9, FUNCT_1:33;
A12: f | X0 c= f by RELAT_1:59;
for z being object st z in (f | X0) " holds
z in f "
proof
let z be object ; :: thesis: ( z in (f | X0) " implies z in f " )
assume A13: z in (f | X0) " ; :: thesis: z in f "
then consider x, y being object such that
A14: z = [x,y] by RELAT_1:def 1;
A15: ( x in dom ((f | X0) ") & y = ((f | X0) ") . x ) by A13, A14, FUNCT_1:1;
A16: x = (f | X0) . y by A6, A7, A15, FUNCT_1:32;
y in rng ((f | X0) ") by A13, A14, XTUPLE_0:def 13;
then A17: [y,x] in f by A7, A12, A16, FUNCT_1:1;
then A18: ( y in dom f & x = f . y ) by FUNCT_1:1;
x in rng f by A17, XTUPLE_0:def 13;
then ( x in dom (f ") & y = (f ") . x ) by A1, A18, FUNCT_1:32;
hence z in f " by A14, FUNCT_1:1; :: thesis: verum
end;
then [x,(((f | X0) ") . x)] in f " by A11, FUNCT_1:1;
hence ((f ") | Y0) . x = ((f | X0) ") . x by A10, FUNCT_1:1; :: thesis: verum
end;
hence (f | X0) " = (f ") | Y0 by A5, A8; :: thesis: verum