let E, F be RealNormSpace; :: thesis: for s, t being Point of [:E,F:]
for a being Real holds
( s = [(s `1),(s `2)] & (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) & (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )
let s, t be Point of [:E,F:]; :: thesis: for a being Real holds
( s = [(s `1),(s `2)] & (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) & (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )
let a be Real; :: thesis: ( s = [(s `1),(s `2)] & (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) & (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )
consider s1 being Point of E, s2 being Point of F such that
A1: s = [s1,s2] by PRVECT_3:18;
consider t1 being Point of E, t2 being Point of F such that
A2: t = [t1,t2] by PRVECT_3:18;
thus s = [(s `1),(s `2)] by A1; :: thesis: ( (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) & (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )
s + t = [((s `1) + (t `1)),((s `2) + (t `2))] by A1, A2, PRVECT_3:18;
hence ( (s + t) `1 = (s `1) + (t `1) & (s + t) `2 = (s `2) + (t `2) ) ; :: thesis: ( (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) & (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )
A3: (- 1) * t = [((- 1) * (t `1)),((- 1) * (t `2))] by A2, PRVECT_3:18
.= [(- (t `1)),((- 1) * (t `2))] by RLVECT_1:16
.= [(- (t `1)),(- (t `2))] by RLVECT_1:16 ;
s - t = s + ((- 1) * t) by RLVECT_1:16
.= [((s `1) - (t `1)),((s `2) - (t `2))] by A1, A3, PRVECT_3:18 ;
hence ( (s - t) `1 = (s `1) - (t `1) & (s - t) `2 = (s `2) - (t `2) ) ; :: thesis: ( (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) )
a * s = [(a * (s `1)),(a * (s `2))] by A1, PRVECT_3:18;
hence ( (a * s) `1 = a * (s `1) & (a * s) `2 = a * (s `2) ) ; :: thesis: verum