let R be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for P, Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3)
for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model
let P, Q be Element of BK_model ; :: thesis: for u, v, w being non zero Element of (TOP-REAL 3)
for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model
let u, v, w be non zero Element of (TOP-REAL 3); :: thesis: for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model
let r be Real; :: thesis: ( 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) implies R is Element of BK_model )
assume that
A1: ( 0 <= r & r <= 1 ) and
A2: ( P = Dir u & Q = Dir v & R = Dir w ) and
A3: ( u . 3 = 1 & v . 3 = 1 ) and
A4: w = (r * u) + ((1 - r) * v) ; :: thesis: R is Element of BK_model
reconsider ru = r * u, rv = (1 - r) * v as Element of REAL 3 by EUCLID:22;
A5: w . 3 = (ru . 3) + (rv . 3) by A4, RVSUM_1:11
.= (r * (u . 3)) + (rv . 3) by RVSUM_1:44
.= r + ((1 - r) * 1) by A3, RVSUM_1:44
.= 1 ;
consider u2 being non zero Element of (TOP-REAL 3) such that
A6: ( Dir u2 = P & u2 . 3 = 1 & BK_to_REAL2 P = |[(u2 . 1),(u2 . 2)]| ) by BKMODEL2:def 2;
A7: u = u2 by A2, A3, A6, Th16;
reconsider ru2 = |[(u2 . 1),(u2 . 2)]| as Element of (TOP-REAL 2) ;
consider v2 being non zero Element of (TOP-REAL 3) such that
A8: ( Dir v2 = Q & v2 . 3 = 1 & BK_to_REAL2 Q = |[(v2 . 1),(v2 . 2)]| ) by BKMODEL2:def 2;
A9: v = v2 by A2, A3, A8, Th16;
reconsider rv2 = |[(v2 . 1),(v2 . 2)]| as Element of (TOP-REAL 2) ;
reconsider rw = |[(w . 1),(w . 2)]| as Element of (TOP-REAL 2) ;
rw = (r * ru2) + ((1 - r) * rv2)

proof

A10: w . 1 = (ru . 1) + (rv . 1) by A4, RVSUM_1:11
.= (r * (u . 1)) + (rv . 1) by RVSUM_1:44
.= (r * (u2 . 1)) + ((1 - r) * (v2 . 1)) by A7, A9, RVSUM_1:44 ;
A13: w . 2 = (ru . 2) + (rv . 2) by A4, RVSUM_1:11
.= (r * (u . 2)) + (rv . 2) by RVSUM_1:44
.= (r * (u2 . 2)) + ((1 - r) * (v2 . 2)) by A7, A9, RVSUM_1:44 ;
(r * ru2) + ((1 - r) * rv2) = |[(r * (u2 . 1)),(r * (u2 . 2))]| + ((1 - r) * |[(v2 . 1),(v2 . 2)]|) by EUCLID:58
.= |[(r * (u2 . 1)),(r * (u2 . 2))]| + |[((1 - r) * (v2 . 1)),((1 - r) * (v2 . 2))]| by EUCLID:58 ;
hence rw = (r * ru2) + ((1 - r) * rv2) by A10, A13, EUCLID:56; :: thesis: verum

end;

then rw = ((1 - r) * rv2) + (r * ru2) ;
then rw in { (((1 - r) * rv2) + (r * ru2)) where r is Real : ( 0 <= r & r <= 1 ) } by A1;
then rw in LSeg (rv2,ru2) by RLTOPSP1:def 2;
then reconsider rw = rw as Element of inside_of_circle (0,0,1) by A6, A8, Th15;
consider RW2 being Element of (TOP-REAL 2) such that
A11: ( RW2 = rw & REAL2_to_BK rw = Dir |[(RW2 `1),(RW2 `2),1]| ) by BKMODEL2:def 3;
A12: ( rw `1 = w . 1 & rw `2 = w . 2 ) by EUCLID:52;
w = |[(w `1),(w `2),(w `3)]| by EUCLID_5:3
.= |[(w . 1),(w `2),(w `3)]| by EUCLID_5:def 1
.= |[(w . 1),(w . 2),(w `3)]| by EUCLID_5:def 2
.= |[(w . 1),(w . 2),(w . 3)]| by EUCLID_5:def 3 ;
hence R is Element of BK_model by A2, A11, A5, A12; :: thesis: verum