let S be RelStr ; :: thesis: for T being non empty RelStr
for f being Function of S,T
for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let T be non empty RelStr ; :: thesis: for f being Function of S,T
for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let f be Function of S,T; :: thesis: for S9 being SubRelStr of S
for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let S9 be SubRelStr of S; :: thesis: for T9 being SubRelStr of T st f .: the carrier of S9 c= the carrier of T9 holds
f | the carrier of S9 is Function of S9,T9
let T9 be SubRelStr of T; :: thesis: ( f .: the carrier of S9 c= the carrier of T9 implies f | the carrier of S9 is Function of S9,T9 )
assume A1: f .: the carrier of S9 c= the carrier of T9 ; :: thesis: f | the carrier of S9 is Function of S9,T9
set g = f | the carrier of S9;
A2: dom f = the carrier of S by FUNCT_2:def 1;
the carrier of S9 c= the carrier of S by YELLOW_0:def 13;
then A3: dom (f | the carrier of S9) = the carrier of S9 by A2, RELAT_1:62;
rng (f | the carrier of S9) = f .: the carrier of S9 by RELAT_1:115;
hence f | the carrier of S9 is Function of S9,T9 by A1, A3, FUNCT_2:2; :: thesis: verum