theorem :: FINSEQ_3:150

for X, Y, Z being set holds Funcs (X,<*Y,Z*>) = <*(Funcs (X,Y)),(Funcs (X,Z))*>