let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V holds Af (AMSpace V,w,y) = Lambda (OASpace V)
let w, y be VECTOR of V; :: thesis: Af (AMSpace V,w,y) = Lambda (OASpace V)
set Y = OASpace V;
( the carrier of (Lambda (OASpace V)) = the carrier of V & the CONGR of (Lambda (OASpace V)) = lambda (DirPar V) ) by Th22, Th23;
hence Af (AMSpace V,w,y) = Lambda (OASpace V) ; :: thesis: verum