let n be Nat; :: thesis: for An being Subset of (TOP-REAL n) st 0* n in An holds
Affin An = [#] (Lin An)
let An be Subset of (TOP-REAL n); :: thesis: ( 0* n in An implies Affin An = [#] (Lin An) )
set TR = TOP-REAL n;
set A = An;
A1: ( 0* n = 0. (TOP-REAL n) & An c= Affin An ) by EUCLID:66, RLAFFIN1:49;
assume 0* n in An ; :: thesis: Affin An = [#] (Lin An)
hence Affin An = (0. (TOP-REAL n)) + (Up (Lin ((- (0. (TOP-REAL n))) + An))) by A1, RLAFFIN1:57
.= Up (Lin ((- (0. (TOP-REAL n))) + An)) by RLAFFIN1:6
.= Up (Lin ((0. (TOP-REAL n)) + An)) by RLVECT_1:12
.= Up (Lin An) by RLAFFIN1:6
.= [#] (Lin An) by RUSUB_4:def 5 ;
:: thesis: verum