let X, Y be non empty set ; :: thesis: for S being SigmaField of X
for T being Function of X,Y
for B being Subset of Y st T is bijective holds
( T " B in S iff B in CopyField (T,S) )
let S be SigmaField of X; :: thesis: for T being Function of X,Y
for B being Subset of Y st T is bijective holds
( T " B in S iff B in CopyField (T,S) )
let T be Function of X,Y; :: thesis: for B being Subset of Y st T is bijective holds
( T " B in S iff B in CopyField (T,S) )
let B be Subset of Y; :: thesis: ( T is bijective implies ( T " B in S iff B in CopyField (T,S) ) )
assume T is bijective ; :: thesis: ( T " B in S iff B in CopyField (T,S) )
then consider H being Function of Y,X such that
A1: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) by Th17;
( B in CopyField (T,S) iff H .: B in CopyField (H,(CopyField (T,S))) ) by Th18, A1;
hence ( T " B in S iff B in CopyField (T,S) ) by A1, FUNCT_1:85; :: thesis: verum