let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for S being Field_Subset of X
for M being Measure of S st f is bijective holds
( ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) )
let f be Function of X,Y; :: thesis: for S being Field_Subset of X
for M being Measure of S st f is bijective holds
( ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) )
let S be Field_Subset of X; :: thesis: for M being Measure of S st f is bijective holds
( ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) )
let M be Measure of S; :: thesis: ( f is bijective implies ( ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) ) )
assume A1: f is bijective ; :: thesis: ( ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) & ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) )
A2: dom ((.: f) | S) = S by FUNCT_2:def 1;
rng ((.: f) | S) = (.: f) .: S by RELAT_1:115;
then A3: rng ((.: f) | S) = CopyField (f,S) by A1, Def1;
then reconsider G = (.: f) | S as Function of S,(CopyField (f,S)) by A2, FUNCT_2:1;
A4: G is one-to-one by A1, FUNCT_1:52;
G is onto by A3, FUNCT_2:def 3;
hence ex G being Function of S,(CopyField (f,S)) st
( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) by A2, A4, A3; :: thesis: ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective )
A5: dom (G ") = CopyField (f,S) by A4, A3, FUNCT_1:33;
A6: rng (G ") = S by A2, A4, FUNCT_1:33;
then reconsider F = G " as Function of (CopyField (f,S)),S by A5, FUNCT_2:1;
F is onto by A6, FUNCT_2:def 3;
hence ex F being Function of (CopyField (f,S)),S st
( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) by A4, A5, A6; :: thesis: verum