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: f .: S is cap-finite-partition-closed Subset-Family of Y

per cases ( f .: S is empty or not f .: S is empty ) ;

suppose f .: S is empty ; :: thesis: f .: S is cap-finite-partition-closed Subset-Family of Y

hence f .: S is cap-finite-partition-closed Subset-Family of Y ; :: thesis: verum

end;

suppose A2: not f .: S is empty ; :: thesis: f .: S is cap-finite-partition-closed Subset-Family of Y

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 b₁ being Element of bool fS st b₁ is a_partition of s1 /\ s2 )
assume A3: not s1 /\ s2 is empty ; :: thesis: ex b₁ being Element of bool fS st b₁ 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 A4, FUNCT_2:def 10;
A7: s2 in fS by A2;
consider c2 being Subset of X such that
A8: c2 in S and
A9: s2 = f .: c2 by A7, FUNCT_2:def 10;
A10: f .: (c1 /\ c2) = s1 /\ s2 by A1, A6, A9, FUNCT_1:62;
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 A5, A8, A11, SRINGS_1:def 1;
( 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 A12, A13, RELAT_1:123;
then t1 c= s1 /\ s2 by A14, A1, A6, A9, FUNCT_1:62;
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 A16, FUNCT_2:def 10;
f .: v c= f .: (c1 /\ c2) by A12, A17, RELAT_1:123;
hence t in s1 /\ s2 by A15, A18, A10; :: 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 A1, A6, A9, FUNCT_1:62;
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 A12, A20, EQREL_1:def 4;
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 A19, A22, FUNCT_1:def 6, A23, FUNCT_2:def 10;
hence t in union (f .: x2) by A21, TARSKI:def 4; :: 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 A26, A29, A12, EQREL_1:def 4, A27, A30, A1, FUNCT_1:66; :: 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;