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));
A1: ( signnorm (f,(v1 - w)) = |.(f . ((v1 - w),(v1 - w))).| & signnorm (f,v1) = |.(f . (v1,v1)).| ) by Th41;
( (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))).| ) by Th41, Th49;
hence |.(f . ((v1 + w),(v1 + w))).| + |.(f . ((v1 - w),(v1 - w))).| = (2 * |.(f . (v1,v1)).|) + (2 * |.(f . (w,w)).|) by A1, Th41; :: thesis: verum