let X be set ; :: thesis: for Y being non empty RelStr
for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
let Y be non empty RelStr ; :: thesis: for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
let x be Element of (Y |^ X); :: thesis: ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
x in the carrier of (Y |^ X) ;
then x in Funcs (X, the carrier of Y) by Th28;
hence ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y ) by FUNCT_2:66; :: thesis: verum