let V be RealLinearSpace; for u, v, x, y being VECTOR of V st Gen x,y holds
Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v))
let u, v, x, y be VECTOR of V; ( Gen x,y implies Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v)) )
assume A1:
Gen x,y
; Orte (x,y,(u + v)) = (Orte (x,y,u)) + (Orte (x,y,v))
hence Orte (x,y,(u + v)) =
((pr2 (x,y,(u + v))) * x) + ((- ((pr1 (x,y,u)) + (pr1 (x,y,v)))) * y)
by Lm7
.=
(((pr2 (x,y,u)) + (pr2 (x,y,v))) * x) + ((- ((pr1 (x,y,u)) + (pr1 (x,y,v)))) * y)
by A1, Lm7
.=
(((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + ((- ((pr1 (x,y,u)) + (pr1 (x,y,v)))) * y)
by RLVECT_1:def 6
.=
(((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + (((pr1 (x,y,u)) + (pr1 (x,y,v))) * (- y))
by RLVECT_1:24
.=
(((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + (- (((pr1 (x,y,u)) + (pr1 (x,y,v))) * y))
by RLVECT_1:25
.=
(((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + (- (((pr1 (x,y,u)) * y) + ((pr1 (x,y,v)) * y)))
by RLVECT_1:def 6
.=
(((pr2 (x,y,u)) * x) + ((pr2 (x,y,v)) * x)) + ((- ((pr1 (x,y,u)) * y)) + (- ((pr1 (x,y,v)) * y)))
by RLVECT_1:31
.=
((pr2 (x,y,u)) * x) + (((pr2 (x,y,v)) * x) + ((- ((pr1 (x,y,u)) * y)) + (- ((pr1 (x,y,v)) * y))))
by RLVECT_1:def 3
.=
((pr2 (x,y,u)) * x) + ((- ((pr1 (x,y,u)) * y)) + (((pr2 (x,y,v)) * x) + (- ((pr1 (x,y,v)) * y))))
by RLVECT_1:def 3
.=
(((pr2 (x,y,u)) * x) + (- ((pr1 (x,y,u)) * y))) + (((pr2 (x,y,v)) * x) + (- ((pr1 (x,y,v)) * y)))
by RLVECT_1:def 3
.=
(((pr2 (x,y,u)) * x) + ((pr1 (x,y,u)) * (- y))) + (((pr2 (x,y,v)) * x) + (- ((pr1 (x,y,v)) * y)))
by RLVECT_1:25
.=
(((pr2 (x,y,u)) * x) + ((pr1 (x,y,u)) * (- y))) + (((pr2 (x,y,v)) * x) + ((pr1 (x,y,v)) * (- y)))
by RLVECT_1:25
.=
(((pr2 (x,y,u)) * x) + ((- (pr1 (x,y,u))) * y)) + (((pr2 (x,y,v)) * x) + ((pr1 (x,y,v)) * (- y)))
by RLVECT_1:24
.=
(Orte (x,y,u)) + (Orte (x,y,v))
by RLVECT_1:24
;
verum