let D be non empty set ; :: thesis: for X being finite set
for Y being non empty finite set
for x being object st not x in X holds
for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds
for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
let X be finite set ; :: thesis: for Y being non empty finite set
for x being object st not x in X holds
for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds
for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
let Y be non empty finite set ; :: thesis: for x being object st not x in X holds
for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds
for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
let x be object ; :: thesis: ( not x in X implies for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds
for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g) )
assume A1: not x in X ; :: thesis: for F being BinOp of D st F is having_a_unity & F is commutative & F is associative holds
for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
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: ( F is having_a_unity & F is commutative & F is associative implies for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g) )
assume that
A6: F is having_a_unity and
A7: F is commutative and
A8: F is associative ; :: thesis: for f being Function of (Funcs (X,Y)),D
for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
let f be Function of (Funcs (X,Y)),D; :: thesis: for g being Function of (Funcs ((X \/ {x}),Y)),D st ( 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 ) holds
F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
let g be Function of (Funcs ((X \/ {x}),Y)),D; :: thesis: ( ( 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 ) implies F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g) )
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: F $$ ((In ((Funcs (X,Y)),(Fin (Funcs (X,Y))))),f) = F $$ ((In ((Funcs ((X \/ {x}),Y)),(Fin (Funcs ((X \/ {x}),Y))))),g)
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))
proof
let z be Element of Funcs (X,Y); :: thesis: f . z = F $$ (Y9,((curry gB) . z))
reconsider Z = z as Function of X,Y ;
set SF = { h where h is Function of (X \/ {x}),Y : h | X = Z } ;
deffunc H1( 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 = H1(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 )
proof
let x9 be object ; :: thesis: ( x9 in ZY iff x9 in q .: Y )
thus ( x9 in ZY implies x9 in q .: Y ) :: thesis: ( x9 in q .: Y implies x9 in ZY )
proof
assume x9 in ZY ; :: thesis: x9 in q .: Y
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: verum
end;
assume x9 in q .: Y ; :: thesis: x9 in ZY
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: verum
end;
then A19: q .: Y = ZY by TARSKI:2;
then A20: rng q = ZY by A10, RELAT_1:113;
now :: thesis: for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 implies x1 = x2 )
assume that
A21: x1 in dom q and
A22: x2 in dom q and
A23: q . x1 = q . x2 ; :: thesis: x1 = x2
A24: q . x2 = [z,x2] by A10, A22;
[z,x1] = q . x1 by A10, A21;
hence x1 = x2 by A23, A24, XTUPLE_0:1; :: thesis: verum
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;
now :: thesis: for x9 being object st x9 in Y holds
C . x9 = gBq . x9
let x9 be object ; :: thesis: ( x9 in Y implies C . x9 = gBq . x9 )
assume A28: x9 in Y ; :: thesis: C . x9 = gBq . x9
A29: q . x9 = [z,x9] by A10, A28;
C . x9 = gB . (z,x9) by A27, A28;
hence C . x9 = gBq . x9 by A28, A29, FUNCT_2:15; :: thesis: verum
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 }
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in B .: ZY or b in { h where h is Function of (X \/ {x}),Y : h | X = Z } )
assume b in B .: ZY ; :: thesis: b in { h where h is Function of (X \/ {x}),Y : h | X = Z }
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: verum
end;
A39: { h where h is Function of (X \/ {x}),Y : h | X = Z } c= B .: ZY
proof
x in {x} by TARSKI:def 1;
then A40: x in X \/ {x} by XBOOLE_0:def 3;
let sf be object ; :: according to TARSKI:def 3 :: thesis: ( not sf in { h where h is Function of (X \/ {x}),Y : h | X = Z } or sf in B .: ZY )
assume sf in { h where h is Function of (X \/ {x}),Y : h | X = Z } ; :: thesis: sf in B .: ZY
then consider h being Function of (X \/ {x}),Y such that
A41: h = sf and
A42: h | X = Z ;
A43: [:(Funcs (X,Y)),Y:] = dom B by FUNCT_2:def 1;
dom h = X \/ {x} by FUNCT_2:def 1;
then A44: h . x in rng h by A40, FUNCT_1:def 3;
A45: rng h c= Y by RELAT_1:def 19;
then A46: [z,(h . x)] in [:(Funcs (X,Y)),Y:] by A44, ZFMISC_1:87;
z in {Z} by TARSKI:def 1;
then [z,(h . x)] in ZY by A44, A45, ZFMISC_1:87;
then B . (z,(h . x)) in B .: ZY by A46, A43, FUNCT_1:def 6;
hence sf in B .: ZY by A3, A41, A42; :: thesis: verum
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: verum
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: verum