let x be Real; :: thesis: for p being Point of (TOP-REAL 3) holds
( (x * p) `1 = x * (p `1 ) & (x * p) `2 = x * (p `2 ) & (x * p) `3 = x * (p `3 ) )
let p be Point of (TOP-REAL 3); :: thesis: ( (x * p) `1 = x * (p `1 ) & (x * p) `2 = x * (p `2 ) & (x * p) `3 = x * (p `3 ) )
A1: (x * p) `1 = |[(x * (p `1 )),(x * (p `2 )),(x * (p `3 ))]| `1 by Th7;
A2: (x * p) `2 = |[(x * (p `1 )),(x * (p `2 )),(x * (p `3 ))]| `2 by Th7;
(x * p) `3 = |[(x * (p `1 )),(x * (p `2 )),(x * (p `3 ))]| `3 by Th7;
hence ( (x * p) `1 = x * (p `1 ) & (x * p) `2 = x * (p `2 ) & (x * p) `3 = x * (p `3 ) ) by A1, A2, FINSEQ_1:62; :: thesis: verum