let F be Field; 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; 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; 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; ( 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
; 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; verum