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;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: p + ((Mx2Tran M) " A) c= (Mx2Tran M) " (((Mx2Tran M) . p) + A)

let x be object ; :: thesis: ( x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) implies x in p + ((Mx2Tran M) " A) )
assume A4: x in (Mx2Tran M) " (((Mx2Tran M) . p) + A) ; :: thesis: x in p + ((Mx2Tran M) " A)
then reconsider f = x as Element of (TOP-REAL n) ;
(Mx2Tran M) . x in ((Mx2Tran M) . p) + A by A4, FUNCT_1:def 7;
then consider v being Element of (TOP-REAL m) such that
A5: (Mx2Tran M) . x = ((Mx2Tran M) . p) + v and
A6: v in A by A2;
((Mx2Tran M) . f) - ((Mx2Tran M) . p) = (v + ((Mx2Tran M) . p)) - ((Mx2Tran M) . p) by A5
.= v + (((Mx2Tran M) . p) - ((Mx2Tran M) . p)) by RLVECT_1:28
.= v + (0. (TOP-REAL m)) by RLVECT_1:15
.= v by RLVECT_1:4 ;
then v = (Mx2Tran M) . (f - p) by Th28;
then A7: f - p in (Mx2Tran M) " A by A3, A6, FUNCT_1:def 7;
p + (f - p) = (f - p) + p
.= f - (p - p) by RLVECT_1:29
.= f - (0. (TOP-REAL n)) by RLVECT_1:15
.= f by RLVECT_1:13 ;
hence x in p + ((Mx2Tran M) " A) by A1, A7; :: thesis: verum

end;

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