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 19, CSSPACE:def 20 ; :: thesis: verum