let X, Y be non empty set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is cap-finite-partition-closed Subset-Family of Y

let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for f being Function of X,Y st f is one-to-one holds
f .: S is cap-finite-partition-closed Subset-Family of Y

let f be Function of X,Y; :: thesis: ( f is one-to-one implies f .: S is cap-finite-partition-closed Subset-Family of Y )
assume A1: f is one-to-one ; :: thesis:
per cases ( f .: S is empty or not f .: S is empty ) ;
suppose f .: S is empty ; :: thesis:
end;
suppose A2: not f .: S is empty ; :: thesis:
reconsider fS = f .: S as Subset-Family of Y ;
fS is cap-finite-partition-closed
proof
let s1, s2 be Element of fS; :: according to SRINGS_1:def 1 :: thesis: ( s1 /\ s2 is empty or ex b1 being Element of bool fS st b1 is a_partition of s1 /\ s2 )
assume A3: not s1 /\ s2 is empty ; :: thesis: ex b1 being Element of bool fS st b1 is a_partition of s1 /\ s2
A4: s1 in fS by A2;
consider c1 being Subset of X such that
A5: c1 in S and
A6: s1 = f .: c1 by ;
A7: s2 in fS by A2;
consider c2 being Subset of X such that
A8: c2 in S and
A9: s2 = f .: c2 by ;
A10: f .: (c1 /\ c2) = s1 /\ s2 by ;
then A11: not c1 /\ c2 is empty by A3;
consider x1 being finite Subset of S such that
A12: x1 is a_partition of c1 /\ c2 by ;
( x1 c= S & S c= bool X ) ;
then x1 c= bool X ;
then reconsider x2 = x1 as Subset-Family of X ;
now :: thesis: ( f .: x2 is finite Subset of fS & f .: x2 is a_partition of s1 /\ s2 )
thus f .: x2 is finite Subset of fS by FUNCT_2:103; :: thesis: f .: x2 is a_partition of s1 /\ s2
thus f .: x2 is a_partition of s1 /\ s2 :: thesis: verum
proof
now :: thesis: ( f .: x2 is Subset-Family of (s1 /\ s2) & union (f .: x2) = s1 /\ s2 & ( for A being Subset of (s1 /\ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) ) ) )
f .: x2 c= bool (s1 /\ s2)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in f .: x2 or t in bool (s1 /\ s2) )
assume t in f .: x2 ; :: thesis: t in bool (s1 /\ s2)
then consider y1 being Subset of X such that
A13: y1 in x2 and
A14: t = f .: y1 by FUNCT_2:def 10;
reconsider t1 = t as set by A14;
f .: y1 c= f .: (c1 /\ c2) by ;
then t1 c= s1 /\ s2 by ;
hence t in bool (s1 /\ s2) ; :: thesis: verum
end;
hence f .: x2 is Subset-Family of (s1 /\ s2) ; :: thesis: ( union (f .: x2) = s1 /\ s2 & ( for A being Subset of (s1 /\ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) ) ) )

now :: thesis: ( ( for t being object st t in union (f .: x2) holds
t in s1 /\ s2 ) & ( for t being object st t in s1 /\ s2 holds
t in union (f .: x2) ) )
hereby :: thesis: for t being object st t in s1 /\ s2 holds
t in union (f .: x2)
let t be object ; :: thesis: ( t in union (f .: x2) implies t in s1 /\ s2 )
assume t in union (f .: x2) ; :: thesis: t in s1 /\ s2
then consider u being set such that
A15: t in u and
A16: u in f .: x2 by TARSKI:def 4;
consider v being Subset of X such that
A17: v in x2 and
A18: u = f .: v by ;
f .: v c= f .: (c1 /\ c2) by ;
hence t in s1 /\ s2 by ; :: thesis: verum
end;
let t be object ; :: thesis: ( t in s1 /\ s2 implies t in union (f .: x2) )
assume t in s1 /\ s2 ; :: thesis: t in union (f .: x2)
then t in f .: (c1 /\ c2) by ;
then consider v being object such that
A19: v in dom f and
A20: v in c1 /\ c2 and
A21: t = f . v by FUNCT_1:def 6;
v in union x1 by ;
then consider u being set such that
A22: v in u and
A23: u in x1 by TARSKI:def 4;
reconsider fu = f .: u as Subset of Y ;
( f . v in f .: u & f .: u in f .: x2 ) by ;
hence t in union (f .: x2) by ; :: thesis: verum
end;
hence union (f .: x2) = s1 /\ s2 by TARSKI:def 3; :: thesis: for A being Subset of (s1 /\ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) )

now :: thesis: for A being Subset of (s1 /\ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) )
let A be Subset of (s1 /\ s2); :: thesis: ( A in f .: x2 implies ( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) ) )

assume A in f .: x2 ; :: thesis: ( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) )

then consider a0 being Subset of X such that
A26: a0 in x2 and
A27: A = f .: a0 by FUNCT_2:def 10;
thus A <> {} :: thesis: for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B )
proof
assume A28: A = {} ; :: thesis: contradiction
dom f = X by PARTFUN1:def 2;
hence contradiction by A26, A12, A28, A27; :: thesis: verum
end;
let B be Subset of (s1 /\ s2); :: thesis: ( not B in f .: x2 or A = B or A misses B )
assume B in f .: x2 ; :: thesis: ( A = B or A misses B )
then consider b0 being Subset of X such that
A29: b0 in x2 and
A30: B = f .: b0 by FUNCT_2:def 10;
thus ( A = B or A misses B ) by ; :: thesis: verum
end;
hence for A being Subset of (s1 /\ s2) st A in f .: x2 holds
( A <> {} & ( for B being Subset of (s1 /\ s2) holds
( not B in f .: x2 or A = B or A misses B ) ) ) ; :: thesis: verum
end;
hence f .: x2 is a_partition of s1 /\ s2 by EQREL_1:def 4; :: thesis: verum
end;
end;
hence ex x being finite Subset of fS st x is a_partition of s1 /\ s2 ; :: thesis: verum
end;
hence f .: S is cap-finite-partition-closed Subset-Family of Y ; :: thesis: verum
end;
end;