let S be set ; :: thesis: for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S,the carrier of T )
let T be non empty RelStr ; :: thesis: for f being set holds
( f is Element of (T |^ S) iff f is Function of S,the carrier of T )
let f be set ; :: thesis: ( f is Element of (T |^ S) iff f is Function of S,the carrier of T )

hereby :: thesis: ( f is Function of S,the carrier of T implies f is Element of (T |^ S) )

assume f is Element of (T |^ S) ; :: thesis: f is Function of S,the carrier of T
then f in the carrier of (T |^ S) ;
then f in Funcs S,the carrier of T by YELLOW_1:28;
then consider a being Function such that
A1: ( a = f & dom a = S & rng a c= the carrier of T ) by FUNCT_2:def 2;
thus f is Function of S,the carrier of T by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

assume f is Function of S,the carrier of T ; :: thesis: f is Element of (T |^ S)
then f in Funcs S,the carrier of T by FUNCT_2:11;
hence f is Element of (T |^ S) by YELLOW_1:28; :: thesis: verum