let X be RealUnitarySpace; :: thesis: for M being Subspace of X

for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

let M be Subspace of X; :: thesis: for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

let x be Point of X; :: thesis: for y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

let y1, y2, z1, z2 be Point of X; :: thesis: ( y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 implies ( y1 = y2 & z1 = z2 ) )

assume that

A1: ( y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M ) and

A2: ( x = y1 + z1 & x = y2 + z2 ) ; :: thesis: ( y1 = y2 & z1 = z2 )

y1 + (z1 + (- y2)) = (y2 + z2) + (- y2) by RLVECT_1:def 3, A2;

then y1 + ((- y2) + z1) = y2 + ((- y2) + z2) by RLVECT_1:def 3;

then (y1 + (- y2)) + z1 = y2 + ((- y2) + z2) by RLVECT_1:def 3;

then (y1 - y2) + z1 = (y2 + (- y2)) + z2 by RLVECT_1:def 3;

then (y1 - y2) + z1 = z2 + (0. X) by RLVECT_1:def 10;

then (y1 - y2) + (z1 + (- z1)) = z2 + (- z1) by RLVECT_1:def 3;

then A31: (y1 - y2) + (0. X) = z2 + (- z1) by RLVECT_1:def 10;

A4: ( y1 - y2 in M & z2 - z1 in Ort_Comp M ) by A1, RUSUB_1:17;

then y1 - y2 in the carrier of M /\ the carrier of (Ort_Comp M) by XBOOLE_0:def 4, A31;

then y1 - y2 = 0. X by Lm814;

hence y1 = y2 by RLVECT_1:21; :: thesis: z1 = z2

z2 - z1 in the carrier of M /\ the carrier of (Ort_Comp M) by A4, A31, XBOOLE_0:def 4;

then z2 - z1 = 0. X by Lm814;

hence z1 = z2 by RLVECT_1:21; :: thesis: verum

for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

let M be Subspace of X; :: thesis: for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

let x be Point of X; :: thesis: for y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

let y1, y2, z1, z2 be Point of X; :: thesis: ( y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 implies ( y1 = y2 & z1 = z2 ) )

assume that

A1: ( y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M ) and

A2: ( x = y1 + z1 & x = y2 + z2 ) ; :: thesis: ( y1 = y2 & z1 = z2 )

y1 + (z1 + (- y2)) = (y2 + z2) + (- y2) by RLVECT_1:def 3, A2;

then y1 + ((- y2) + z1) = y2 + ((- y2) + z2) by RLVECT_1:def 3;

then (y1 + (- y2)) + z1 = y2 + ((- y2) + z2) by RLVECT_1:def 3;

then (y1 - y2) + z1 = (y2 + (- y2)) + z2 by RLVECT_1:def 3;

then (y1 - y2) + z1 = z2 + (0. X) by RLVECT_1:def 10;

then (y1 - y2) + (z1 + (- z1)) = z2 + (- z1) by RLVECT_1:def 3;

then A31: (y1 - y2) + (0. X) = z2 + (- z1) by RLVECT_1:def 10;

A4: ( y1 - y2 in M & z2 - z1 in Ort_Comp M ) by A1, RUSUB_1:17;

then y1 - y2 in the carrier of M /\ the carrier of (Ort_Comp M) by XBOOLE_0:def 4, A31;

then y1 - y2 = 0. X by Lm814;

hence y1 = y2 by RLVECT_1:21; :: thesis: z1 = z2

z2 - z1 in the carrier of M /\ the carrier of (Ort_Comp M) by A4, A31, XBOOLE_0:def 4;

then z2 - z1 = 0. X by Lm814;

hence z1 = z2 by RLVECT_1:21; :: thesis: verum