let F be Field; :: thesis: for S being OrtSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ a,b,(l * x) = l * (ProJ a,b,x)
let S be OrtSp of F; :: thesis: for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ a,b,(l * x) = l * (ProJ a,b,x)
let b, a, x be Element of S; :: thesis: for l being Element of F st not a _|_ holds
ProJ a,b,(l * x) = l * (ProJ a,b,x)
let l be Element of F; :: thesis: ( not a _|_ implies ProJ a,b,(l * x) = l * (ProJ a,b,x) )
set L = x - ((ProJ a,b,x) * b);
A1: l * (x - ((ProJ a,b,x) * b)) = (l * x) - (l * ((ProJ a,b,x) * b)) by VECTSP_1:70
.= (l * x) - ((l * (ProJ a,b,x)) * b) by VECTSP_1:def 28 ;
assume A2: not a _|_ ; :: thesis: ProJ a,b,(l * x) = l * (ProJ a,b,x)
then A3: a _|_ by Th24;
a _|_ by A2, Th24;
then a _|_ by A1, Def2;
hence ProJ a,b,(l * x) = l * (ProJ a,b,x) by A2, A3, Th20; :: thesis: verum