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 consider f' being Function such that
A1: ( f' = sup F & dom f' = the carrier of S & rng f' c= the carrier of T ) by FUNCT_2:def 2;
thus sup F is Function of S,T by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum