let X, Y be non empty set ; :: thesis: for S being SigmaField of X
for T being Function of X,Y
for A being Subset of X st T is bijective holds
( A in S iff T .: A in CopyField (T,S) )
let S be SigmaField of X; :: thesis: for T being Function of X,Y
for A being Subset of X st T is bijective holds
( A in S iff T .: A in CopyField (T,S) )
let T be Function of X,Y; :: thesis: for A being Subset of X st T is bijective holds
( A in S iff T .: A in CopyField (T,S) )
let A be Subset of X; :: thesis: ( T is bijective implies ( A in S iff T .: A in CopyField (T,S) ) )
assume A1: T is bijective ; :: thesis: ( A in S iff T .: A in CopyField (T,S) )
A2: dom (.: T) = bool X by FUNCT_2:def 1;
consider H being Function of Y,X such that
A3: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) by A1, Th17;
A4: dom (.: H) = bool Y by FUNCT_2:def 1;

hereby :: thesis: ( T .: A in CopyField (T,S) implies A in S )

assume A in S ; :: thesis: T .: A in CopyField (T,S)
then (.: T) . A in (.: T) .: S by A2, FUNCT_1:def 6;
then (.: T) . A in CopyField (T,S) by A1, Def2;
hence T .: A in CopyField (T,S) by A1, Th1; :: thesis: verum

end;

assume T .: A in CopyField (T,S) ; :: thesis: A in S
then (.: T) . A in CopyField (T,S) by A1, Th1;
then (.: H) . ((.: T) . A) in (.: H) .: (CopyField (T,S)) by A4, FUNCT_1:def 6;
hence A in S by A2, A3, FUNCT_1:34; :: thesis: verum