set v = the Element of X1;
the Element of X1 in X1 by A1;
then reconsider v = the Element of X1 as Element of X ;
v - v = 0. X by RLVECT_1:15;
hence 0. X is Element of X1 by A1, RLSUB_1:3; :: thesis: verum