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 by Th22;
hence Af (AMSpace (V,w,y)) = Lambda (OASpace V) by Th23; :: thesis: verum