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_{1}[ 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_{1}[I] & not i in I holds

S_{1}[I \/ {i}]
_{1}[ {}. X]
_{1}[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

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

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

S

proof

A36:
S
let A be Element of Fin X; :: thesis: for i being Element of X st S_{1}[A] & not i in A holds

S_{1}[A \/ {i}]

let a be Element of X; :: thesis: ( S_{1}[A] & not a in A implies S_{1}[A \/ {a}] )

assume that

A6: S_{1}[A]
and

A7: not a in A ; :: thesis: S_{1}[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

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;

end;S

let a be Element of X; :: thesis: ( S

assume that

A6: S

A7: not a in A ; :: thesis: S

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

then A14:
F $$ (A,(g * f)) = F $$ ((f .: A),g)
by A6;
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;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

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

end;

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

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;

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

then A26:
F $$ ((f .: I),g) = F . ((F $$ ((f .: A),g)),((g * f) . a))
by A2, A3, A16, A18, SETWOP_2:2;
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;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

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

then A33:
union (f .: A) misses f . a
by ZFMISC_1:80;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;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

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

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

proof

for I being Element of Fin X holds S
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;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

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