let D be non empty set ; :: thesis:
let X be finite set ; :: thesis:
let Y be non empty finite set ; :: thesis:
let x be object ; :: 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;
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 FINSUB_1:def 5;
reconsider FXY9 = Funcs (X,Y) as Element of Fin (Funcs (X,Y)) by FINSUB_1:def 5;
Funcs ((X \/ {x}),Y) in Fin (Funcs ((X \/ {x}),Y)) by FINSUB_1:def 5;
then A5: In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y)))) = Funcs ((X \/ {x}),Y) by SUBSET_1:def 8;
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₁( object ) -> object = [z,$1];
consider q being Function such that
A10: ( dom q = Y & ( for x being object st x in Y holds
q . x = H₁(x) ) ) from FUNCT_1:sch 3();
A11: {z} c= Funcs (X,Y) by ZFMISC_1:31;
then [:{Z},Y:] c= [:(Funcs (X,Y)),Y:] by ZFMISC_1:95;
then reconsider ZY = [:{Z},Y:] as Element of Fin [:(Funcs (X,Y)),Y:] by FINSUB_1:def 5;
for x9 being object holds
( x9 in ZY iff x9 in q .: Y )

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

assume x9 in ZY ; :: thesis:
then consider z9, y9 being object 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 6; :: thesis:

end;

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

end;

end;

then A25: q is one-to-one by FUNCT_1:def 4;
ZY c= [:(Funcs (X,Y)),Y:] by A11, ZFMISC_1:95;
then reconsider q = q as Function of Y,[:(Funcs (X,Y)),Y:] by A10, A20, FUNCT_2:2;
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 object st y9 in Y holds
C . y9 = gB . (z,y9) by FUNCT_5:29;
reconsider C = C as Function of Y,D by A26;

end;

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

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in B .: ZY ; :: thesis:
then consider zy being object such that
zy in dom B and
A32: zy in ZY and
A33: b = B . zy by FUNCT_1:def 6;
consider z9, y9 being object 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:40;
then consider F1 being Function of (X \/ {x}),Y such that
A37: F1 | X = Z and
A38: F1 . x = y9 by A1, STIRL2_1:57;
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;
then A47: F $$ ((B .: ZY),g) = f . Z by A9;
F $$ ((B .: ZY),g) = F $$ (ZY,gB) by A7, A8, A2, SETWOP_2:6;
hence f . z = F $$ (Y9,((curry gB) . z)) by A7, A8, A47, A25, A19, A26, A30, SETWOP_2:6; :: thesis:

end;

then F $$ ([:FXY9,Y9:],gB) = F $$ (FXY9,f) by A6, A7, A8, MATRIX_3:30;
then A48: F $$ (domB,gB) = F $$ (FXY9,f) by FUNCT_2:def 1;
A49: rng B = Funcs ((X \/ {x}),Y) by A2, FUNCT_2:def 3;
F $$ ((B .: domB),g) = F $$ (domB,(g * B)) by A7, A8, A2, SETWOP_2:6;
then F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g) = F $$ (domB,(g * B)) by A49, A5, RELAT_1:113;
hence F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g) by A48; :: thesis: