let D be non empty set ; :: thesis:
let X be finite set ; :: thesis:
let Y be non empty finite set ; :: thesis:
let x be set ; :: thesis:
assume A1: not x in X ; :: thesis:
set Xx = X \/ {x};
set FXY = Funcs X,Y;
set FXxY = Funcs (X \/ {x}),Y;
consider B being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) such that
A2: B is bijective and
A3: for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
B . f,(F . x) = F by A1, Th57;
A4: Funcs X,Y is finite by FRAENKEL:16;
dom B = [:(Funcs X,Y),Y:] by FUNCT_2:def 1;
then reconsider domB = dom B as Element of Fin [:(Funcs X,Y),Y:] by A4, FINSUB_1:def 5;
Funcs X,Y is finite by FRAENKEL:16;
then reconsider FXY9 = Funcs X,Y as Element of Fin (Funcs X,Y) by FINSUB_1:def 5;
A5: FinOmega (Funcs (X \/ {x}),Y) = Funcs (X \/ {x}),Y by FRAENKEL:16, MATRIX_2:def 17;
reconsider Y9 = Y as Element of Fin Y by FINSUB_1:def 5;
let F be BinOp of D; :: thesis:
assume that
A6: F is having_a_unity and
A7: F is commutative and
A8: F is associative ; :: thesis:
let f be Function of (Funcs X,Y),D; :: thesis:
let g be Function of (Funcs (X \/ {x}),Y),D; :: thesis:
assume A9: for H being Function of X,Y
for SF being Element of Fin (Funcs (X \/ {x}),Y) st SF = { h where h is Function of (X \/ {x}),Y : h | X = H } holds
F $$ SF,g = f . H ; :: thesis:
reconsider gB = g * B as Function of [:(Funcs X,Y),Y:],D ;
for z being Element of Funcs X,Y holds f . z = F $$ Y9,((curry gB) . z)

let z be Element of Funcs X,Y; :: thesis:
reconsider Z = z as Function of X,Y ;
set SF = { h where h is Function of (X \/ {x}),Y : h | X = Z } ;
deffunc H₁( set ) -> set = [z,$1];
consider q being Function such that
A10: ( dom q = Y & ( for x being set st x in Y holds
q . x = H₁(x) ) ) from FUNCT_1:sch 3();
A11: {z} c= Funcs X,Y by ZFMISC_1:37;
then [:{Z},Y:] c= [:(Funcs X,Y),Y:] by ZFMISC_1:118;
then reconsider ZY = [:{Z},Y:] as Element of Fin [:(Funcs X,Y),Y:] by FINSUB_1:def 5;
for x9 being set holds
( x9 in ZY iff x9 in q .: Y )

let x9 be set ; :: thesis:
thus ( x9 in ZY implies x9 in q .: Y ) :: thesis:

assume x9 in ZY ; :: thesis:
then consider z9, y9 being set such that
A12: z9 in {Z} and
A13: y9 in Y and
A14: x9 = [z9,y9] by ZFMISC_1:def 2;
A15: z = z9 by A12, TARSKI:def 1;
q . y9 = [z,y9] by A10, A13;
hence x9 in q .: Y by A10, A13, A14, A15, FUNCT_1:def 12; :: thesis:

end;

assume x9 in q .: Y ; :: thesis:
then consider y9 being set such that
A16: y9 in dom q and
A17: y9 in Y and
A18: x9 = q . y9 by FUNCT_1:def 12;
x9 = [z,y9] by A10, A16, A18;
hence x9 in ZY by A17, ZFMISC_1:128; :: thesis:

end;

let x1, x2 be set ; :: thesis:
assume that
A21: x1 in dom q and
A22: x2 in dom q and
A23: q . x1 = q . x2 ; :: thesis:
A24: q . x2 = [z,x2] by A10, A22;
[z,x1] = q . x1 by A10, A21;
hence x1 = x2 by A23, A24, ZFMISC_1:33; :: thesis:

end;

then A25: q is one-to-one by FUNCT_1:def 8;
ZY c= [:(Funcs X,Y),Y:] by A11, ZFMISC_1:118;
then reconsider q = q as Function of Y,[:(Funcs X,Y),Y:] by A10, A20, FUNCT_2:4;
reconsider gBq = gB * q as Function of Y,D ;
dom gB = [:(Funcs X,Y),Y:] by FUNCT_2:def 1;
then consider C being Function such that
A26: (curry gB) . z = C and
dom C = Y and
rng C c= rng gB and
A27: for y9 being set st y9 in Y holds
C . y9 = gB . z,y9 by FUNCT_5:36;
reconsider C = C as Function of Y,D by A26;

end;

then A30: C = gBq by FUNCT_2:18;
A31: B .: ZY c= { h where h is Function of (X \/ {x}),Y : h | X = Z }

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in B .: ZY ; :: thesis:
then consider zy being set such that
zy in dom B and
A32: zy in ZY and
A33: b = B . zy by FUNCT_1:def 12;
consider z9, y9 being set such that
A34: z9 in {Z} and
A35: y9 in Y and
A36: zy = [z9,y9] by A32, ZFMISC_1:def 2;
Y \/ {y9} = Y by A35, ZFMISC_1:46;
then consider F1 being Function of (X \/ {x}),Y such that
A37: F1 | X = Z and
A38: F1 . x = y9 by A1, STIRL2_1:67;
z9 = Z by A34, TARSKI:def 1;
then B . z9,y9 = F1 by A3, A37, A38;
hence b in { h where h is Function of (X \/ {x}),Y : h | X = Z } by A33, A36, A37; :: thesis:

end;

end;

then reconsider SF = { h where h is Function of (X \/ {x}),Y : h | X = Z } as Element of Fin (Funcs (X \/ {x}),Y) by A31, XBOOLE_0:def 10;
B .: ZY = SF by A31, A39, XBOOLE_0:def 10;
then A47: F $$ (B .: ZY),g = f . Z by A9;
F $$ (B .: ZY),g = F $$ ZY,gB by A7, A8, A2, SETWOP_2:8;
hence f . z = F $$ Y9,((curry gB) . z) by A7, A8, A47, A25, A19, A26, A30, SETWOP_2:8; :: thesis:

end;