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 ex a being Function st
( a = f & dom a = S & rng a c= the carrier of T ) by FUNCT_2:def 2;
hence f is Function of S, the carrier of T by FUNCT_2:def 1, RELSET_1:4; :: 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:8;
hence f is Element of (T |^ S) by YELLOW_1:28; :: thesis: verum