o in rng the charact of S ;
then ( o <> {} & o in PFuncs (( the carrier of S *), the carrier of S) ) by RELAT_1:def 9;
then ( o . a in rng o & rng o c= the carrier of S ) by RELAT_1:def 19, FUNCT_1:3;
hence o . a is Element of S ; :: thesis: verum