let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||
let x, y be Point of X; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
Re ((x + y) .|. (x + y)) >= 0 by Def13;
then A1: |.((x + y) .|. (x + y)).| >= 0 by Th36;
A2: ||.(x + y).|| ^2 >= 0 by XREAL_1:65;
sqrt (||.(x + y).|| ^2 ) = sqrt |.((x + y) .|. (x + y)).| by Th46, SQUARE_1:89;
then A3: ||.(x + y).|| ^2 = |.((x + y) .|. (x + y)).| by A1, A2, SQUARE_1:96;
A4: Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = (Re (((x .|. x) + (x .|. y)) + (y .|. x))) + (Re (y .|. y)) by COMPLEX1:19
.= ((Re ((x .|. x) + (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y)) by COMPLEX1:19
.= (((Re (x .|. x)) + (Re (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y)) by COMPLEX1:19
.= ((|.(x .|. x).| + (Re (x .|. y))) + (Re (y .|. x))) + (Re (y .|. y)) by Th36
.= ((|.(x .|. x).| + (Re (x .|. y))) + (Re (y .|. x))) + |.(y .|. y).| by Th36 ;
A5: Re (x .|. y) = Re ((x .|. y) *' ) by COMPLEX1:112
.= Re (y .|. x) by Def13 ;
A6: Im ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = (Im (((x .|. x) + (x .|. y)) + (y .|. x))) + (Im (y .|. y)) by COMPLEX1:19
.= ((Im ((x .|. x) + (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y)) by COMPLEX1:19
.= (((Im (x .|. x)) + (Im (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y)) by COMPLEX1:19
.= ((0 + (Im (x .|. y))) + (Im (y .|. x))) + (Im (y .|. y)) by Def13
.= ((Im (x .|. y)) + (Im (y .|. x))) + 0 by Def13 ;
A7: - (Im (x .|. y)) = Im ((x .|. y) *' ) by COMPLEX1:112
.= Im (y .|. x) by Def13 ;
Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) = Re ((x + y) .|. (x + y)) by Th33;
then A8: Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)) >= 0 by Def13;
(((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y) = (Re ((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y))) + (0 * <i> ) by A6, A7, COMPLEX1:29;
then |.((((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)).| = (|.(x .|. x).| + (2 * (Re (x .|. y)))) + |.(y .|. y).| by A4, A5, A8, ABSVALUE:def 1;
then A9: ||.(x + y).|| ^2 = (2 * (Re (x .|. y))) + (|.(x .|. x).| + |.(y .|. y).|) by A3, Th33;
|.(x .|. x).| >= 0 by COMPLEX1:132;
then A10: (sqrt |.(x .|. x).|) ^2 = |.(x .|. x).| by SQUARE_1:def 4;
|.(y .|. y).| >= 0 by COMPLEX1:132;
then A11: |.(y .|. y).| = ||.y.|| ^2 by SQUARE_1:def 4;
( Re (x .|. y) <= |.(x .|. y).| & |.(x .|. y).| <= ||.x.|| * ||.y.|| ) by Th37, COMPLEX1:140;
then Re (x .|. y) <= ||.x.|| * ||.y.|| by XXREAL_0:2;
then 2 * (Re (x .|. y)) <= 2 * (||.x.|| * ||.y.||) by XREAL_1:66;
then ||.(x + y).|| ^2 <= (2 * (||.x.|| * ||.y.||)) + ((||.x.|| ^2 ) + |.(y .|. y).|) by A9, A10, XREAL_1:8;
then A12: ||.(x + y).|| ^2 <= (||.x.|| + ||.y.||) ^2 by A11;
( ||.x.|| >= 0 & ||.y.|| >= 0 ) by Th46;
then ||.x.|| + ||.y.|| >= 0 + 0 by XREAL_1:9;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A12, SQUARE_1:78; :: thesis: verum