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

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