let F be Field; :: thesis: for S being OrtSp of F
for a, b, 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 a, b, 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 a, b, 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:23
.= (l * x) - ((l * (ProJ (a,b,x))) * b) by VECTSP_1:def 16 ;
assume A2: not a _|_ ; :: thesis: ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
then A3: a _|_ by Th11;
a _|_ by A2, Th11;
then a _|_ by A1, Def1;
hence ProJ (a,b,(l * x)) = l * (ProJ (a,b,x)) by A2, A3, Th8; :: thesis: verum