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 _|_ & l <> 0. F holds

ProJ (a,(l * b),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 _|_ & l <> 0. F holds

ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

let a, b, x be Element of S; :: thesis: for l being Element of F st not a _|_ & l <> 0. F holds

ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

let l be Element of F; :: thesis: ( not a _|_ & l <> 0. F implies ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) )

assume that

A1: not a _|_ and

A2: l <> 0. F ; :: thesis: ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

set L = x - ((ProJ (a,(l * b),x)) * (l * b));

not a _|_ by A1, A2, Th5;

then A3: a _|_ by Th11;

A4: x - ((ProJ (a,(l * b),x)) * (l * b)) = x - (((ProJ (a,(l * b),x)) * l) * b) by VECTSP_1:def 16;

a _|_ by A1, Th11;

then (ProJ (a,b,x)) * (l ") = ((ProJ (a,(l * b),x)) * l) * (l ") by A1, A3, A4, Th8;

then (ProJ (a,b,x)) * (l ") = (ProJ (a,(l * b),x)) * (l * (l ")) by GROUP_1:def 3;

then (l ") * (ProJ (a,b,x)) = (ProJ (a,(l * b),x)) * (1_ F) by A2, VECTSP_1:def 10;

hence ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) ; :: thesis: verum

for a, b, x being Element of S

for l being Element of F st not a _|_ & l <> 0. F holds

ProJ (a,(l * b),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 _|_ & l <> 0. F holds

ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

let a, b, x be Element of S; :: thesis: for l being Element of F st not a _|_ & l <> 0. F holds

ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

let l be Element of F; :: thesis: ( not a _|_ & l <> 0. F implies ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) )

assume that

A1: not a _|_ and

A2: l <> 0. F ; :: thesis: ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

set L = x - ((ProJ (a,(l * b),x)) * (l * b));

not a _|_ by A1, A2, Th5;

then A3: a _|_ by Th11;

A4: x - ((ProJ (a,(l * b),x)) * (l * b)) = x - (((ProJ (a,(l * b),x)) * l) * b) by VECTSP_1:def 16;

a _|_ by A1, Th11;

then (ProJ (a,b,x)) * (l ") = ((ProJ (a,(l * b),x)) * l) * (l ") by A1, A3, A4, Th8;

then (ProJ (a,b,x)) * (l ") = (ProJ (a,(l * b),x)) * (l * (l ")) by GROUP_1:def 3;

then (l ") * (ProJ (a,b,x)) = (ProJ (a,(l * b),x)) * (1_ F) by A2, VECTSP_1:def 10;

hence ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) ; :: thesis: verum