let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b being Element of (DTrSpace V,w,y) st Gen w,y holds
ex p being Element of (DTrSpace V,w,y) st p # a = b
let w, y be VECTOR of V; :: thesis: for a, b being Element of (DTrSpace V,w,y) st Gen w,y holds
ex p being Element of (DTrSpace V,w,y) st p # a = b
let a, b be Element of (DTrSpace V,w,y); :: thesis: ( Gen w,y implies ex p being Element of (DTrSpace V,w,y) st p # a = b )
assume Gen w,y ; :: thesis: ex p being Element of (DTrSpace V,w,y) st p # a = b
reconsider u = a, v = b as VECTOR of V ;
consider u1 being VECTOR of V such that
A1: u # u1 = v by Th7;
reconsider p = u1 as Element of (DTrSpace V,w,y) ;
p # a = u # u1 by Def8;
hence ex p being Element of (DTrSpace V,w,y) st p # a = b by A1; :: thesis: verum