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 ((l * a),b,x) = 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 ((l * a),b,x) = 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 ((l * a),b,x) = ProJ (a,b,x)

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

assume that

A1: not a _|_ and

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

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

then l * a _|_ by Th11;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by Th2;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by Def1;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by VECTSP_1:def 16;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by A2, VECTSP_1:def 10;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by VECTSP_1:def 17;

then A3: a _|_ by Th2;

a _|_ by A1, Th11;

hence ProJ ((l * a),b,x) = ProJ (a,b,x) by A1, A3, Th8; :: thesis: verum

for a, b, x being Element of S

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

ProJ ((l * a),b,x) = 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 ((l * a),b,x) = 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 ((l * a),b,x) = ProJ (a,b,x)

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

assume that

A1: not a _|_ and

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

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

then l * a _|_ by Th11;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by Th2;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by Def1;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by VECTSP_1:def 16;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by A2, VECTSP_1:def 10;

then x - ((ProJ ((l * a),b,x)) * b) _|_ by VECTSP_1:def 17;

then A3: a _|_ by Th2;

a _|_ by A1, Th11;

hence ProJ ((l * a),b,x) = ProJ (a,b,x) by A1, A3, Th8; :: thesis: verum