let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V
for v, w being Element of V holds |.(f . (v + w),(v + w)).| + |.(f . (v - w),(v - w)).| = (2 * |.(f . v,v).|) + (2 * |.(f . w,w).|)
let f be diagReR+0valued hermitan-Form of V; :: thesis: for v, w being Element of V holds |.(f . (v + w),(v + w)).| + |.(f . (v - w),(v - w)).| = (2 * |.(f . v,v).|) + (2 * |.(f . w,w).|)
let v1, w be Element of V; :: thesis: |.(f . (v1 + w),(v1 + w)).| + |.(f . (v1 - w),(v1 - w)).| = (2 * |.(f . v1,v1).|) + (2 * |.(f . w,w).|)
set s1 = signnorm f,v1;
set s2 = signnorm f,w;
set sp = signnorm f,(v1 + w);
set sm = signnorm f,(v1 - w);
( (signnorm f,(v1 + w)) + (signnorm f,(v1 - w)) = (2 * (signnorm f,v1)) + (2 * (signnorm f,w)) & signnorm f,(v1 + w) = |.(f . (v1 + w),(v1 + w)).| & signnorm f,(v1 - w) = |.(f . (v1 - w),(v1 - w)).| & signnorm f,v1 = |.(f . v1,v1).| ) by Th44, Th52;
hence |.(f . (v1 + w),(v1 + w)).| + |.(f . (v1 - w),(v1 - w)).| = (2 * |.(f . v1,v1).|) + (2 * |.(f . w,w).|) by Th44; :: thesis: verum