let S, T be RelStr ; :: thesis: for R being SubRelStr of S
for f being Function of the carrier of S, the carrier of T holds
( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
let R be SubRelStr of S; :: thesis: for f being Function of the carrier of S, the carrier of T holds
( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
let f be Function of the carrier of S, the carrier of T; :: thesis: ( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )
the carrier of R c= the carrier of S by YELLOW_0:def 13;
hence f | R = f | the carrier of R by TMAP_1:def 3; :: thesis: for x being set st x in the carrier of R holds
(f | R) . x = f . x
hence for x being set st x in the carrier of R holds
(f | R) . x = f . x by FUNCT_1:49; :: thesis: verum