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';
A2: dom f = the carrier of S by FUNCT_2:def 1;
the carrier of S' c= the carrier of S by YELLOW_0:def 13;
then A3: dom (f | the carrier of S') = the carrier of S' by A2, RELAT_1:91;
rng (f | the carrier of S') = f .: the carrier of S' by RELAT_1:148;
hence f | the carrier of S' is Function of S',T' by A1, A3, FUNCT_2:4; :: thesis: verum