let r be Real; :: thesis: for V being RealLinearSpace
for y, z being Point of V
for x being object st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
let V be RealLinearSpace; :: thesis: for y, z being Point of V
for x being object st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
let y, z be Point of V; :: thesis: for x being object st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )
let x be object ; :: thesis: ( x = ((1 - r) * y) + (r * z) implies ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) )
assume A1: x = ((1 - r) * y) + (r * z) ; :: thesis: ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )

hereby :: thesis: ( ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) )

assume x = y ; :: thesis: ( r = 0 or y = z )
then 0. V = (((1 - r) * y) + (r * z)) - y by A1, RLVECT_1:5
.= (((1 - r) * y) - y) + (r * z) by RLVECT_1:def 3
.= (((1 - r) * y) - (1 * y)) + (r * z) by RLVECT_1:def 8
.= (((1 - r) - 1) * y) + (r * z) by RLVECT_1:35
.= (r * z) - (r * y) by RLVECT_1:79
.= r * (z - y) by RLVECT_1:34 ;
then ( r = 0 or z - y = 0. V ) by RLVECT_1:11;
hence ( r = 0 or y = z ) by RLVECT_1:21; :: thesis: verum

end;

hereby :: thesis: ( x = z iff ( r = 1 or y = z ) )

assume A2: ( r = 0 or y = z ) ; :: thesis: x = y

per cases ( r = 0 or z = y ) by A2;

suppose r = 0 ; :: thesis: x = y

hence x = y + (0 * z) by A1, RLVECT_1:def 8
.= y + (0. V) by RLVECT_1:10
.= y by RLVECT_1:4 ;
:: thesis: verum

end;

suppose z = y ; :: thesis: x = y

hence x = ((1 - r) + r) * y by A1, RLVECT_1:def 6
.= y by RLVECT_1:def 8 ;
:: thesis: verum

end;

end;

end;

hereby :: thesis: ( ( r = 1 or y = z ) implies x = z )

assume x = z ; :: thesis: ( r = 1 or y = z )
then 0. V = (((1 - r) * y) + (r * z)) - z by A1, RLVECT_1:5
.= ((1 - r) * y) + ((r * z) - z) by RLVECT_1:def 3
.= ((1 - r) * y) + ((r * z) + ((- 1) * z)) by RLVECT_1:16
.= ((1 - r) * y) + (((- 1) + r) * z) by RLVECT_1:def 6
.= ((1 - r) * y) + ((- (1 - r)) * z)
.= ((1 - r) * y) - ((1 - r) * z) by RLVECT_1:79
.= (1 - r) * (y - z) by RLVECT_1:34 ;
then ( (1 - r) + r = 0 + r or y - z = 0. V ) by RLVECT_1:11;
hence ( r = 1 or y = z ) by RLVECT_1:21; :: thesis: verum

end;

assume A3: ( r = 1 or y = z ) ; :: thesis: x = z

per cases ( r = 1 or y = z ) by A3;

suppose r = 1 ; :: thesis: x = z

hence x = (0. V) + (1 * z) by A1, RLVECT_1:10
.= 1 * z by RLVECT_1:4
.= z by RLVECT_1:def 8 ;
:: thesis: verum

end;

suppose y = z ; :: thesis: x = z

hence x = ((1 - r) + r) * z by A1, RLVECT_1:def 6
.= z by RLVECT_1:def 8 ;
:: thesis: verum

end;

end;