for D being non empty set
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)