let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v1, v2 being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
let W be Subspace of V; :: thesis: for v1, v2 being VECTOR of V
for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
let v1, v2 be VECTOR of V; :: thesis: for w1, w2 being VECTOR of W st w1 = v1 & w2 = v2 holds
w1 .|. w2 = v1 .|. v2
let w1, w2 be VECTOR of W; :: thesis: ( w1 = v1 & w2 = v2 implies w1 .|. w2 = v1 .|. v2 )
reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3;
assume ( w1 = v1 & w2 = v2 ) ; :: thesis: w1 .|. w2 = v1 .|. v2
then A1: v1 .|. v2 = the scalar of V . [ww1,ww2] ;
w1 .|. w2 = the scalar of W . [w1,w2]
.= ( the scalar of V || the carrier of W) . [w1,w2] by Def1 ;
hence w1 .|. w2 = v1 .|. v2 by A1, FUNCT_1:49; :: thesis: verum