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