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 FXY = Funcs X,Y;
set Xx = X \/ {x};
set FXxY = Funcs (X \/ {x}),Y;
let F be BinOp of D; :: thesis:
assume A2: ( F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp ) ; :: thesis:
let f be Function of (Funcs X,Y),D; :: thesis:
let g be Function of (Funcs (X \/ {x}),Y),D; :: thesis:
assume A3: 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:
consider B being Function of [:(Funcs X,Y),Y:],(Funcs (X \/ {x}),Y) such that
A4: B is bijective and
A5: 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;
Funcs X,Y is finite by FRAENKEL:16;
then ( dom B = [:(Funcs X,Y),Y:] & [:(Funcs X,Y),Y:] is finite ) by FUNCT_2:def 1;
then reconsider domB = dom B as Element of Fin [:(Funcs X,Y),Y:] by FINSUB_1:def 5;
( B is one-to-one & B is onto & Funcs (X \/ {x}),Y is finite ) by A4, FRAENKEL:16;
then ( F $$ (B .: domB),g = F $$ domB,(g * B) & rng B = Funcs (X \/ {x}),Y & FinOmega (Funcs (X \/ {x}),Y) = Funcs (X \/ {x}),Y ) by A2, FUNCT_2:def 3, MATRIX_2:def 17, SETWOP_2:8;
then A6: F $$ (FinOmega (Funcs (X \/ {x}),Y)),g = F $$ domB,(g * B) by RELAT_1:146;
reconsider Y' = Y as Element of Fin Y by FINSUB_1:def 5;
Funcs X,Y is finite by FRAENKEL:16;
then reconsider FXY' = Funcs X,Y as Element of Fin (Funcs X,Y) by FINSUB_1:def 5;
reconsider gB = g * B as Function of [:(Funcs X,Y),Y:],D ;
for z being Element of Funcs X,Y holds f . z = F $$ Y',((curry gB) . z)

proof

let z be Element of Funcs X,Y; :: thesis:
reconsider Z = z as Function of X,Y by FUNCT_2:121;
set SF = { h where h is Function of (X \/ {x}),Y : h | X = Z } ;
A7: {z} c= Funcs X,Y by ZFMISC_1:37;
then ( [:{Z},Y:] c= [:(Funcs X,Y),Y:] & [:{Z},Y:] is finite ) by ZFMISC_1:118;
then reconsider ZY = [:{Z},Y:] as Element of Fin [:(Funcs X,Y),Y:] by FINSUB_1:def 5;
A8: B .: ZY c= { h where h is Function of (X \/ {x}),Y : h | X = Z }

proof

let b be set ; :: according to TARSKI:def 3 :: thesis:
assume A9: b in B .: ZY ; :: thesis:
consider zy being set such that
A10: ( zy in dom B & zy in ZY & b = B . zy ) by A9, FUNCT_1:def 12;
consider z', y' being set such that
A11: ( z' in {Z} & y' in Y & zy = [z',y'] ) by A10, ZFMISC_1:def 2;
Y \/ {y'} = Y by A11, ZFMISC_1:46;
then consider F1 being Function of (X \/ {x}),Y such that
A12: ( F1 | X = Z & F1 . x = y' ) by A1, STIRL2_1:67;
z' = Z by A11, TARSKI:def 1;
then ( B . z',y' = F1 & F1 in { h where h is Function of (X \/ {x}),Y : h | X = Z } ) by A5, A12;
hence b in { h where h is Function of (X \/ {x}),Y : h | X = Z } by A10, A11; :: thesis:

end;

A13: { h where h is Function of (X \/ {x}),Y : h | X = Z } c= B .: ZY

proof

let sf be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: sf in { h where h is Function of (X \/ {x}),Y : h | X = Z } ; :: thesis:
consider h being Function of (X \/ {x}),Y such that
A15: ( h = sf & h | X = Z ) by A14;
x in {x} by TARSKI:def 1;
then ( x in X \/ {x} & dom h = X \/ {x} ) by FUNCT_2:def 1, XBOOLE_0:def 3;
then ( h . x in rng h & rng h c= Y & z in {Z} ) by FUNCT_1:def 5, RELAT_1:def 19, TARSKI:def 1;
then ( [z,(h . x)] in [:(Funcs X,Y),Y:] & [:(Funcs X,Y),Y:] = dom B & [z,(h . x)] in ZY ) by FUNCT_2:def 1, ZFMISC_1:106;
then B . z,(h . x) in B .: ZY by FUNCT_1:def 12;
hence sf in B .: ZY by A5, A15; :: thesis:

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 A8, XBOOLE_0:def 10;
( B is one-to-one & B .: ZY = SF ) by A4, A8, A13, XBOOLE_0:def 10;
then A16: ( F $$ (B .: ZY),g = f . Z & F $$ (B .: ZY),g = F $$ ZY,gB ) by A2, A3, SETWOP_2:8;
deffunc H₁( set ) -> set = [z,$1];
consider q being Function such that
A17: ( dom q = Y & ( for x being set st x in Y holds
q . x = H₁(x) ) ) from FUNCT_1:sch 3();
A18: q is one-to-one

proof

now

let x1, x2 be set ; :: thesis:
assume A19: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 ) ; :: thesis:
( [z,x1] = q . x1 & q . x2 = [z,x2] ) by A17, A19;
hence x1 = x2 by A19, ZFMISC_1:33; :: thesis:

end;

hence q is one-to-one by FUNCT_1:def 8; :: thesis:

end;

A20: q .: Y = ZY

proof

for x' being set holds
( x' in ZY iff x' in q .: Y )

proof

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

proof

assume x' in ZY ; :: thesis:
then consider z', y' being set such that
A21: ( z' in {Z} & y' in Y & x' = [z',y'] ) by ZFMISC_1:def 2;
( q . y' = [z,y'] & z = z' ) by A17, A21, TARSKI:def 1;
hence x' in q .: Y by A17, A21, FUNCT_1:def 12; :: thesis:

end;

assume x' in q .: Y ; :: thesis:
then consider y' being set such that
A22: ( y' in dom q & y' in Y & x' = q . y' ) by FUNCT_1:def 12;
x' = [z,y'] by A17, A22;
hence x' in ZY by A22, ZFMISC_1:128; :: thesis:

end;

hence q .: Y = ZY by TARSKI:2; :: thesis:

end;

then ( ZY c= [:(Funcs X,Y),Y:] & rng q = ZY ) by A7, A17, RELAT_1:146, ZFMISC_1:118;
then reconsider q = q as Function of Y,[:(Funcs X,Y),Y:] by A17, 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
A23: ( (curry gB) . z = C & dom C = Y & rng C c= rng gB ) and
A24: for y' being set st y' in Y holds
C . y' = gB . z,y' by FUNCT_5:36;
reconsider C = C as Function of Y,D by A23;

now

let x' be set ; :: thesis:
assume A25: x' in Y ; :: thesis:
( C . x' = gB . z,x' & q . x' = [z,x'] & (gB * q) . x' = gB . (q . x') ) by A17, A24, A25, FUNCT_2:21;
hence C . x' = gBq . x' ; :: thesis:

end;

then C = gBq by FUNCT_2:18;
hence f . z = F $$ Y',((curry gB) . z) by A2, A16, A18, A20, A23, SETWOP_2:8; :: thesis:

end;

then F $$ [:FXY',Y':],gB = F $$ FXY',f by A2, MATRIX_3:32;
then ( F $$ domB,gB = F $$ FXY',f & Funcs X,Y is finite ) by FUNCT_2:def 1;
hence F $$ (FinOmega (Funcs X,Y)),f = F $$ (FinOmega (Funcs (X \/ {x}),Y)),g by A6, MATRIX_2:def 17; :: thesis: