let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for S being SigmaField of X st f is bijective holds
(.: f) .: S is SigmaField of Y
let f be Function of X,Y; :: thesis: for S being SigmaField of X st f is bijective holds
(.: f) .: S is SigmaField of Y
let S be SigmaField of X; :: thesis: ( f is bijective implies (.: f) .: S is SigmaField of Y )
set S1 = (.: f) .: S;
assume A1: f is bijective ; :: thesis: (.: f) .: S is SigmaField of Y
then .: f is bijective by Th1;
then A2: ( dom (.: f) = bool X & rng (.: f) = bool Y ) by FUNCT_2:def 1, FUNCT_2:def 3;
A3: ( f is one-to-one & f is onto ) by A1;
reconsider S1 = (.: f) .: S as Field_Subset of Y by A1, Th2;
for A1 being SetSequence of Y st rng A1 c= S1 holds
Intersection A1 in S1

proof

let A1 be SetSequence of Y; :: thesis: ( rng A1 c= S1 implies Intersection A1 in S1 )
assume A4: rng A1 c= S1 ; :: thesis: Intersection A1 in S1
defpred S₁[ set , object ] means ( A1 . $1 = (.: f) . $2 & $2 in S );
A5: for x being Element of NAT ex y being Element of bool X st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of bool X st S₁[x,y]
reconsider B = A1 . x as Subset of Y ;
B in rng A1 by FUNCT_2:4;
then consider z being object such that
A6: ( z in dom (.: f) & z in S & B = (.: f) . z ) by A4, FUNCT_1:def 6;
reconsider z = z as Element of bool X by A6;
take z ; :: thesis: S₁[x,z]
thus (.: f) . z = A1 . x by A6; :: thesis: z in S
thus z in S by A6; :: thesis: verum

end;

consider T being Function of NAT,(bool X) such that
A7: for x being Element of NAT holds S₁[x,T . x] from FUNCT_2:sch 3(A5);
reconsider T = T as SetSequence of X ;

now :: thesis: for s being object st s in rng T holds
s in S

let s be object ; :: thesis: ( s in rng T implies s in S )
assume s in rng T ; :: thesis: s in S
then ex n being Element of NAT st
( n in dom T & s = T . n ) by PARTFUN1:3;
hence s in S by A7; :: thesis: verum

end;

then A8: rng T c= S ;
for y being object holds
( y in f .: (Intersection T) iff y in Intersection A1 )

proof

let y be object ; :: thesis: ( y in f .: (Intersection T) iff y in Intersection A1 )

hereby :: thesis: ( y in Intersection A1 implies y in f .: (Intersection T) )

assume y in f .: (Intersection T) ; :: thesis: y in Intersection A1
then consider x being object such that
A9: ( x in dom f & x in Intersection T & y = f . x ) by FUNCT_1:def 6;

now :: thesis: for n being Nat holds y in A1 . n

let n be Nat; :: thesis: y in A1 . n
A10: x in T . n by PROB_1:13, A9;
n in NAT by ORDINAL1:def 12;
then ( A1 . n = (.: f) . (T . n) & T . n in S ) by A7;
then A1 . n = f .: (T . n) by A1, Th1;
hence y in A1 . n by A9, A10, FUNCT_1:def 6; :: thesis: verum

end;

hence y in Intersection A1 by PROB_1:13; :: thesis: verum

end;

assume A11: y in Intersection A1 ; :: thesis: y in f .: (Intersection T)
then A12: y in A1 . 0 by PROB_1:13;
A13: ( A1 . 0 = (.: f) . (T . 0) & T . 0 in S ) by A7;
(.: f) . (T . 0) = f .: (T . 0) by A1, Th1;
then consider t0 being object such that
A14: ( t0 in dom f & t0 in T . 0 & y = f . t0 ) by A12, A13, FUNCT_1:def 6;

now :: thesis: for n being Nat holds t0 in T . n

let n be Nat; :: thesis: t0 in T . n
A15: y in A1 . n by A11, PROB_1:13;
n in NAT by ORDINAL1:def 12;
then A1 . n = (.: f) . (T . n) by A7;
then A1 . n = f .: (T . n) by A1, Th1;
then ex tn being object st
( tn in dom f & tn in T . n & y = f . tn ) by A15, FUNCT_1:def 6;
hence t0 in T . n by A3, A14; :: thesis: verum

end;

then t0 in Intersection T by PROB_1:13;
hence y in f .: (Intersection T) by A14, FUNCT_1:def 6; :: thesis: verum

end;

then f .: (Intersection T) = Intersection A1 by TARSKI:2;
then A16: (.: f) . (Intersection T) = Intersection A1 by A1, Th1;
Intersection T in S by A8, PROB_1:def 6;
hence Intersection A1 in S1 by A2, A16, FUNCT_1:def 6; :: thesis: verum

end;

then S1 is sigma-multiplicative ;
hence (.: f) .: S is SigmaField of Y ; :: thesis: verum