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 set 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 set 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 set 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 set 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 & F is having_a_unity & g . {} = the_unity_wrt F ) ; :: thesis: for I being Element of Fin X st ( for x, y being set 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 set 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 );
A3: S₁[ {}. X]

proof

let I be Element of Fin X; :: thesis: ( I = {}. X & ( for x, y being set 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
A4: {}. X = I and
for x, y being set 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 )
f .: I = {}. (Fin Y) by A4, RELAT_1:149;
then ( F $$ I,(g * f) = g . {} & union (f .: I) = {} & F $$ (f .: I),g = g . {} & {} c= Y ) by A2, A4, SETWISEO:40, XBOOLE_1:2, ZFMISC_1:2;
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 FINSUB_1:def 5; :: thesis: verum

end;

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 A6: ( S₁[A] & not a in A ) ; :: thesis: S₁[A \/ {a}]
let I be Element of Fin X; :: thesis: ( I = A \/ {a} & ( for x, y being set 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
A7: A \/ {a} = I and
A8: for x, y being set 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 )
A9: for x, y being set st x in A & y in A & f . x meets f . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in A & y in A & f . x meets f . y implies x = y )
assume A10: ( x in A & y in A & f . x meets f . y ) ; :: thesis: x = y
A c= I by A7, XBOOLE_1:7;
hence x = y by A8, A10; :: thesis: verum

end;

then A11: ( F $$ A,(g * f) = F $$ (f .: A),g & F $$ (f .: A),g = g . (union (f .: A)) & union (f .: A) is Element of Fin Y ) by A6;
dom f = X by FUNCT_2:def 1;
then ( Im f,a = {(f . a)} & dom (g * f) = X ) by FUNCT_1:117, FUNCT_2:def 1;
then A12: ( f .: I = (f .: A) \/ {(f . a)} & g . (f . a) = (g * f) . a ) by A7, FUNCT_1:22, RELAT_1:153;

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 A13: ( 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

assume A14: f . a in f .: A ; :: thesis: contradiction
then consider x being set such that
A15: ( x in dom f & x in A & f . x = f . a ) by FUNCT_1:def 12;
( a in {a} & {a} c= I & A c= I ) by A7, TARSKI:def 1, XBOOLE_1:7;
then ( f . x meets f . a & a in I & x in I ) by A13, A14, A15, XBOOLE_1:66;
hence contradiction by A6, A8, A15; :: thesis: verum

end;

then A16: ( F $$ (f .: I),g = F . (F $$ (f .: A),g),((g * f) . a) & F $$ I,(g * f) = F . (F $$ A,(g * f)),((g * f) . a) ) by A2, A6, A7, A12, SETWOP_2:4;
( f . a c= Y & f . a is finite & union (f .: A) c= Y & union (f .: A) is finite ) by A11, FINSUB_1:def 5;
then A17: ( (union (f .: A)) \/ (f . a) c= Y & (union (f .: A)) \/ (f . a) is finite ) by XBOOLE_1:8;
A18: union (f .: I) = (union (f .: A)) \/ (union {(f . a)}) by A12, ZFMISC_1:96
.= (union (f .: A)) \/ (f . a) by ZFMISC_1:31 ;

now

let x be set ; :: thesis: ( x in f .: A implies not x meets f . a )
assume A19: x in f .: A ; :: thesis: not x meets f . a
consider y being set such that
A20: ( y in dom f & y in A & f . y = x ) by A19, FUNCT_1:def 12;
assume A21: x meets f . a ; :: thesis: contradiction
( a in {a} & {a} c= I & A c= I ) by A7, TARSKI:def 1, XBOOLE_1:7;
hence contradiction by A6, A8, A20, A21; :: thesis: verum

end;

then union (f .: A) misses f . a by ZFMISC_1:98;
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, A11, A12, A16, A17, A18, FINSUB_1:def 5; :: thesis: verum

end;

suppose A22: ( 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 A23: ( F is having_a_unity & (f .: A) \/ {(f . a)} = f .: A ) by A2, ZFMISC_1:46;
F $$ I,(g * f) = F . (F $$ (f .: A),g),(the_unity_wrt F) by A2, A6, A7, A11, A12, A22, SETWOP_2:4
.= F $$ (f .: I),g by A12, A23, SETWISEO:23 ;
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, A9, A12, A23; :: thesis: verum

end;

end;

end;

for I being Element of Fin X holds S₁[I] from SETWISEO:sch 2(A3, A5);
hence for I being Element of Fin X st ( for x, y being set 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