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

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 )
;

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

end;fS is cap-finite-partition-closed

proof

hence
f .: S is cap-finite-partition-closed Subset-Family of Y
; :: thesis: verum
let s1, s2 be Element of fS; :: according to SRINGS_1:def 1 :: thesis: ( s1 /\ s2 is empty or ex b_{1} being Element of bool fS st b_{1} is a_partition of s1 /\ s2 )

assume A3: not s1 /\ s2 is empty ; :: thesis: ex b_{1} being Element of bool fS st b_{1} 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 ;

end;assume A3: not s1 /\ s2 is empty ; :: thesis: ex b

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 )

hence
ex x being finite Subset of fS st x is a_partition of s1 /\ s2
; :: thesis: verumthus
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

end;thus f .: x2 is a_partition of s1 /\ s2 :: thesis: verum

proof

end;

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 ) ) ) ) )

hence
f .: x2 is a_partition of s1 /\ s2
by EQREL_1:def 4; :: thesis: verum( 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)

( A <> {} & ( for B being Subset of (s1 /\ s2) holds

( not B in f .: x2 or A = B or A misses B ) ) ) ) )

( A <> {} & ( for B being Subset of (s1 /\ s2) holds

( not B in f .: x2 or A = B or A misses B ) ) )

( A <> {} & ( for B being Subset of (s1 /\ s2) holds

( not B in f .: x2 or A = B or A misses B ) ) ) ; :: thesis: verum

end;proof

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
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;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

( 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) ) )

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 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 s1 /\ s2 implies t in union (f .: x2) )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;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

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

( 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 ) ) )

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 ) ) )

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 )

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;( 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

let B be Subset of (s1 /\ s2); :: thesis: ( not B in f .: x2 or A = B or A misses B )
assume A28:
A = {}
; :: thesis: contradiction

dom f = X by PARTFUN1:def 2;

hence contradiction by A26, A12, A28, A27; :: thesis: verum

end;dom f = X by PARTFUN1:def 2;

hence contradiction by A26, A12, A28, A27; :: thesis: verum

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

( A <> {} & ( for B being Subset of (s1 /\ s2) holds

( not B in f .: x2 or A = B or A misses B ) ) ) ; :: thesis: verum