let D be non empty set ; :: thesis: for p being non empty trivial Sequence of D ex x being Element of D st p = <%x%>
let p be non empty trivial Sequence of D; :: thesis: ex x being Element of D st p = <%x%>
consider x being object such that
A1: p = <%x%> by Th9;
rng p = {x} by A1, AFINSQ_1:33;
then x in rng p by TARSKI:def 1;
then reconsider x = x as Element of D ;
take x ; :: thesis: p = <%x%>
thus p = <%x%> by A1; :: thesis: verum