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) )
assume A1: not a _|_ ; :: thesis: ProJ a,b,(l * x) = l * (ProJ a,b,x)
set L = x - ((ProJ a,b,x) * b);
A2: a _|_ by A1, Th24;
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 26 ;
then A3: a _|_ by A2, Def2;
a _|_ by A1, Th24;
hence ProJ a,b,(l * x) = l * (ProJ a,b,x) by A1, A3, Th20; :: thesis: verum