set a = the Element of A;
reconsider t = <* the Element of A*> as RedSequence of R by REWRITE1:6;
take t ; :: thesis: t is A -valued
thus t is A -valued ; :: thesis: verum