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

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