let a be object ; :: thesis: for A being set st <*a*> is A -valued holds
a in A
let A be set ; :: thesis: ( <*a*> is A -valued implies a in A )
assume A1: <*a*> is A -valued ; :: thesis: a in A
A2: rng <*a*> = {a} by FINSEQ_1:38;
a in {a} by TARSKI:def 1;
hence a in A by A1, A2; :: thesis: verum