let X, Y be non empty set ; :: thesis: for S being SigmaField of X
for T being Function of X,Y st T is bijective holds
ex H being Function of Y,X st
( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )
let S be SigmaField of X; :: thesis: for T being Function of X,Y st T is bijective holds
ex H being Function of Y,X st
( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )
let T be Function of X,Y; :: thesis: ( T is bijective implies ex H being Function of Y,X st
( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) )
assume A1: T is bijective ; :: thesis: ex H being Function of Y,X st
( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )
then .: T is bijective by Th1;
then A2: ( dom (.: T) = bool X & rng (.: T) = bool Y ) by FUNCT_2:def 1, FUNCT_2:def 3;
consider H being Function of Y,X such that
A3: ( H is bijective & H = T " & .: H = (.: T) " ) by A1, Th14;
take H ; :: thesis: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )
thus ( H is bijective & H = T " & H " = T & .: H = (.: T) " ) by A1, A3, FUNCT_1:43; :: thesis: ( (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S )
(.: H) .: (CopyField (T,S)) = (.: H) .: ((.: T) .: S) by A1, Def2;
then (.: H) .: (CopyField (T,S)) = (.: T) " ((.: T) .: S) by A1, A3, FUNCT_1:85;
hence (.: H) .: (CopyField (T,S)) = S by A1, A2, FUNCT_1:94; :: thesis: CopyField (H,(CopyField (T,S))) = S
hence CopyField (H,(CopyField (T,S))) = S by A3, Def2; :: thesis: verum