let S be RelStr ; :: thesis: for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
let T be non empty RelStr ; :: thesis: for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
let F be Subset of (T |^ the carrier of S); :: thesis: sup F is Function of S,T
set f = sup F;
sup F in the carrier of (T |^ the carrier of S) ;
then sup F in Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28;
then ex f9 being Function st
( f9 = sup F & dom f9 = the carrier of S & rng f9 c= the carrier of T ) by FUNCT_2:def 2;
hence sup F is Function of S,T by FUNCT_2:def 1, RELSET_1:4; :: thesis: verum