let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for S being Field_Subset of X st f is bijective holds
(.: f) .: S is Field_Subset of Y
let f be Function of X,Y; :: thesis: for S being Field_Subset of X st f is bijective holds
(.: f) .: S is Field_Subset of Y
let S be Field_Subset of X; :: thesis: ( f is bijective implies (.: f) .: S is Field_Subset of Y )
assume A1: f is bijective ; :: thesis: (.: f) .: S is Field_Subset 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: ( dom f = X & rng f = Y ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
reconsider S1 = (.: f) .: S as Subset-Family of Y ;
A4: for A, B being set st A in S1 & B in S1 holds
A /\ B in S1

proof

let A, B be set ; :: thesis: ( A in S1 & B in S1 implies A /\ B in S1 )
assume A5: ( A in S1 & B in S1 ) ; :: thesis: A /\ B in S1
then consider s being object such that
A6: ( s in dom (.: f) & s in S & A = (.: f) . s ) by FUNCT_1:def 6;
consider t being object such that
A7: ( t in dom (.: f) & t in S & B = (.: f) . t ) by FUNCT_1:def 6, A5;
reconsider s = s, t = t as Subset of X by A6, A7;
A8: ( (.: f) . s = f .: s & (.: f) . t = f .: t ) by A1, Th1;
(f .: s) /\ (f .: t) = f .: (s /\ t) by A1, FUNCT_1:62;
then A9: A /\ B = (.: f) . (s /\ t) by A1, A6, A7, A8, Th1;
s /\ t in S by FINSUB_1:def 2, A6, A7;
hence A /\ B in S1 by A2, A9, FUNCT_1:def 6; :: thesis: verum

end;

for A being Subset of Y st A in S1 holds
A ` in S1

proof

let A be Subset of Y; :: thesis: ( A in S1 implies A ` in S1 )
assume A in S1 ; :: thesis: A ` in S1
then consider s being object such that
A10: ( s in dom (.: f) & s in S & A = (.: f) . s ) by FUNCT_1:def 6;
reconsider s = s as Subset of X by A10;
A11: (.: f) . s = f .: s by A1, Th1;
f .: (s `) = (f .: X) \ (f .: s) by A1, FUNCT_1:64;
then f .: (s `) = Y \ (f .: s) by RELAT_1:113, A3;
then A12: (.: f) . (s `) = A ` by A1, A10, A11, Th1;
s ` in S by A10, PROB_1:def 1;
hence A ` in S1 by A2, A12, FUNCT_1:def 6; :: thesis: verum

end;

then ( not S1 is empty & S1 is cap-closed & S1 is compl-closed ) by A2, A4, FINSUB_1:def 2;
hence (.: f) .: S is Field_Subset of Y ; :: thesis: verum