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) _|_ ;
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