let n, m be Nat; :: thesis: for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
let p be Point of (TOP-REAL n); :: thesis: for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
let M be Matrix of n,m,F_Real; :: thesis: for A being Subset of (TOP-REAL m) holds (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
set MT = Mx2Tran M;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be Subset of (TOP-REAL m); :: thesis: (Mx2Tran M) " (((Mx2Tran M) . p) + A) = p + ((Mx2Tran M) " A)
set w = p;
set MTw = (Mx2Tran M) . p;
A1: p + ((Mx2Tran M) " A) = { (p + v) where v is Element of (TOP-REAL n) : v in (Mx2Tran M) " A } by RUSUB_4:def 8;
A2: ((Mx2Tran M) . p) + A = { (((Mx2Tran M) . p) + v) where v is Element of (TOP-REAL m) : v in A } by RUSUB_4:def 8;
A3: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p + ((Mx2Tran M) " A) or x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) )
assume x in p + ((Mx2Tran M) " A) ; :: thesis: x in (Mx2Tran M) " (((Mx2Tran M) . p) + A)
then consider v being Element of (TOP-REAL n) such that
A8: x = p + v and
A9: v in (Mx2Tran M) " A by A1;
A10: (Mx2Tran M) . v in A by A9, FUNCT_1:def 7;
(Mx2Tran M) . (p + v) = ((Mx2Tran M) . p) + ((Mx2Tran M) . v) by Th27;
then (Mx2Tran M) . x in ((Mx2Tran M) . p) + A by A2, A8, A10;
hence x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) by A3, A8, FUNCT_1:def 7; :: thesis: verum