let X, Y, D be non empty set ; :: thesis: for f being Function of X,(Fin Y)
for g being Function of (Fin Y),D
for F being BinOp of D st ( for A, B being Element of Fin Y st A misses B holds
F . ((g . A),(g . B)) = g . (A \/ B) ) & F is commutative & F is associative & F is having_a_unity & g . {} = the_unity_wrt F holds
for I being Element of Fin X st ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )
let f be Function of X,(Fin Y); :: thesis: for g being Function of (Fin Y),D
for F being BinOp of D st ( for A, B being Element of Fin Y st A misses B holds
F . ((g . A),(g . B)) = g . (A \/ B) ) & F is commutative & F is associative & F is having_a_unity & g . {} = the_unity_wrt F holds
for I being Element of Fin X st ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )
let g be Function of (Fin Y),D; :: thesis: for F being BinOp of D st ( for A, B being Element of Fin Y st A misses B holds
F . ((g . A),(g . B)) = g . (A \/ B) ) & F is commutative & F is associative & F is having_a_unity & g . {} = the_unity_wrt F holds
for I being Element of Fin X st ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )
let F be BinOp of D; :: thesis: ( ( for A, B being Element of Fin Y st A misses B holds
F . ((g . A),(g . B)) = g . (A \/ B) ) & F is commutative & F is associative & F is having_a_unity & g . {} = the_unity_wrt F implies for I being Element of Fin X st ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) )
assume that
A1: for A, B being Element of Fin Y st A misses B holds
F . ((g . A),(g . B)) = g . (A \/ B) and
A2: ( F is commutative & F is associative ) and
A3: F is having_a_unity and
A4: g . {} = the_unity_wrt F ; :: thesis: for I being Element of Fin X st ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )
defpred S₁[ set ] means for I being Element of Fin X st I = $1 & ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y );
A5: for I being Element of Fin X
for i being Element of X st S₁[I] & not i in I holds
S₁[I \/ {i}]

proof

let A be Element of Fin X; :: thesis: for i being Element of X st S₁[A] & not i in A holds
S₁[A \/ {i}]
let a be Element of X; :: thesis: ( S₁[A] & not a in A implies S₁[A \/ {a}] )
assume that
A6: S₁[A] and
A7: not a in A ; :: thesis: S₁[A \/ {a}]
let I be Element of Fin X; :: thesis: ( I = A \/ {a} & ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) implies ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) )
assume that
A8: A \/ {a} = I and
A9: for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ; :: thesis: ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )
A10: for x, y being object st x in A & y in A & f . x meets f . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in A & y in A & f . x meets f . y implies x = y )
assume that
A11: x in A and
A12: y in A and
A13: f . x meets f . y ; :: thesis: x = y
A c= I by A8, XBOOLE_1:7;
hence x = y by A9, A11, A12, A13; :: thesis: verum

end;

then A14: F $$ (A,(g * f)) = F $$ ((f .: A),g) by A6;
A15: union (f .: A) is Element of Fin Y by A6, A10;
dom f = X by FUNCT_2:def 1;
then Im (f,a) = {(f . a)} by FUNCT_1:59;
then A16: f .: I = (f .: A) \/ {(f . a)} by A8, RELAT_1:120;
A17: F $$ ((f .: A),g) = g . (union (f .: A)) by A6, A10;
dom (g * f) = X by FUNCT_2:def 1;
then A18: g . (f . a) = (g * f) . a by FUNCT_1:12;

per cases ( not f . a is empty or not f . a in f .: A or ( f . a is empty & f . a in f .: A ) ) ;

suppose A19: ( not f . a is empty or not f . a in f .: A ) ; :: thesis: ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )

not f . a in f .: A

proof

A20: A c= I by A8, XBOOLE_1:7;
A21: {a} c= I by A8, XBOOLE_1:7;
A22: a in {a} by TARSKI:def 1;
assume A23: f . a in f .: A ; :: thesis: contradiction
then consider x being object such that
x in dom f and
A24: x in A and
A25: f . x = f . a by FUNCT_1:def 6;
f . x meets f . a by A19, A23, A25, XBOOLE_1:66;
hence contradiction by A7, A9, A24, A22, A21, A20; :: thesis: verum

end;

then A26: F $$ ((f .: I),g) = F . ((F $$ ((f .: A),g)),((g * f) . a)) by A2, A3, A16, A18, SETWOP_2:2;
A27: f . a c= Y by FINSUB_1:def 5;
union (f .: A) c= Y by A15, FINSUB_1:def 5;
then A28: (union (f .: A)) \/ (f . a) c= Y by A27, XBOOLE_1:8;

now :: thesis: for x being set st x in f .: A holds
not x meets f . a

let x be set ; :: thesis: ( x in f .: A implies not x meets f . a )
assume x in f .: A ; :: thesis: not x meets f . a
then A29: ex y being object st
( y in dom f & y in A & f . y = x ) by FUNCT_1:def 6;
A30: a in {a} by TARSKI:def 1;
A31: A c= I by A8, XBOOLE_1:7;
A32: {a} c= I by A8, XBOOLE_1:7;
assume x meets f . a ; :: thesis: contradiction
hence contradiction by A7, A9, A29, A30, A32, A31; :: thesis: verum

end;

then A33: union (f .: A) misses f . a by ZFMISC_1:80;
union (f .: I) = (union (f .: A)) \/ (union {(f . a)}) by A16, ZFMISC_1:78
.= (union (f .: A)) \/ (f . a) by ZFMISC_1:25 ;
hence ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) by A1, A2, A3, A7, A8, A14, A17, A15, A18, A26, A28, A33, FINSUB_1:def 5, SETWOP_2:2; :: thesis: verum

end;

suppose A34: ( f . a is empty & f . a in f .: A ) ; :: thesis: ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )

then A35: (f .: A) \/ {(f . a)} = f .: A by ZFMISC_1:40;
F $$ (I,(g * f)) = F . ((F $$ ((f .: A),g)),(the_unity_wrt F)) by A2, A3, A4, A7, A8, A14, A18, A34, SETWOP_2:2
.= F $$ ((f .: I),g) by A3, A16, A35, SETWISEO:15 ;
hence ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) by A6, A10, A16, A35; :: thesis: verum

end;

end;

end;

A36: S₁[ {}. X]

proof

A37: {} c= Y ;
let I be Element of Fin X; :: thesis: ( I = {}. X & ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) implies ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) )
assume that
A38: {}. X = I and
for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ; :: thesis: ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y )
A39: f .: I = {}. (Fin Y) by A38;
F $$ (I,(g * f)) = g . {} by A2, A3, A4, A38, SETWISEO:31;
hence ( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) by A2, A3, A4, A39, A37, FINSUB_1:def 5, SETWISEO:31, ZFMISC_1:2; :: thesis: verum

end;

for I being Element of Fin X holds S₁[I] from SETWISEO:sch 2(A36, A5);
hence for I being Element of Fin X st ( for x, y being object st x in I & y in I & f . x meets f . y holds
x = y ) holds
( F $$ (I,(g * f)) = F $$ ((f .: I),g) & F $$ ((f .: I),g) = g . (union (f .: I)) & union (f .: I) is Element of Fin Y ) ; :: thesis: verum