reconsider t = p . i as context of x by B;
take t ; :: thesis: t in rng p
thus t in rng p by B, FUNCT_1:def 3; :: thesis: verum