let S be RelStr ; :: thesis: for T being non empty RelStr
for f being Function of S,T
for S' being SubRelStr of S
for T' being SubRelStr of T st f .: the carrier of S' c= the carrier of T' holds
f | the carrier of S' is Function of S',T'
let T be non empty RelStr ; :: thesis: for f being Function of S,T
for S' being SubRelStr of S
for T' being SubRelStr of T st f .: the carrier of S' c= the carrier of T' holds
f | the carrier of S' is Function of S',T'
let f be Function of S,T; :: thesis: for S' being SubRelStr of S
for T' being SubRelStr of T st f .: the carrier of S' c= the carrier of T' holds
f | the carrier of S' is Function of S',T'
let S' be SubRelStr of S; :: thesis: for T' being SubRelStr of T st f .: the carrier of S' c= the carrier of T' holds
f | the carrier of S' is Function of S',T'
let T' be SubRelStr of T; :: thesis: ( f .: the carrier of S' c= the carrier of T' implies f | the carrier of S' is Function of S',T' )
assume A1: f .: the carrier of S' c= the carrier of T' ; :: thesis: f | the carrier of S' is Function of S',T'
set g = f | the carrier of S';
( dom f = the carrier of S & the carrier of S' c= the carrier of S ) by FUNCT_2:def 1, YELLOW_0:def 13;
then ( dom (f | the carrier of S') = the carrier of S' & rng (f | the carrier of S') = f .: the carrier of S' ) by RELAT_1:91, RELAT_1:148;
hence f | the carrier of S' is Function of S',T' by A1, FUNCT_2:4; :: thesis: verum