let v, w be VECTOR of Complex_l2_Space; :: thesis: v .|. w = Sum ((seq_id v) (#) ((seq_id w) *'))
thus v .|. w = the scalar of Complex_l2_Space . (v,w) by CSSPACE:def 12
.= Sum ((seq_id v) (#) ((seq_id w) *')) by CSSPACE:def 17, CSSPACE:def 18 ; :: thesis: verum