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