let u, v be VECTOR of Complex_l2_Space; :: thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by Lm12
.= (seq_id u) - (seq_id v) by Lm14 ; :: thesis: verum