let R be RelStr ; :: thesis: for T being non empty 1-sorted
for p being Element of T holds the carrier of (R --> p) = the carrier of R
let T be non empty 1-sorted ; :: thesis: for p being Element of T holds the carrier of (R --> p) = the carrier of R
let p be Element of T; :: thesis: the carrier of (R --> p) = the carrier of R
RelStr(# the carrier of (R --> p),the InternalRel of (R --> p) #) = RelStr(# the carrier of R,the InternalRel of R #) by Def7;
hence the carrier of (R --> p) = the carrier of R ; :: thesis: verum