take v = <*> REAL; :: thesis: v is constant
let n be Nat; :: according to SEQM_3:def 10 :: thesis: for m being Nat st n in dom v & m in dom v holds
v . n = v . m
let m be Nat; :: thesis: ( n in dom v & m in dom v implies v . n = v . m )
assume that
n in dom v and
m in dom v ; :: thesis: v . n = v . m
thus v . n = v . m ; :: thesis: verum