let n be Element of NAT ; :: thesis: for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let RAS be ReperAlgebra of n; :: thesis: for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let a, b be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let W be ATLAS of RAS; :: thesis: for v being Vector of W
for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let v be Vector of W; :: thesis: for x being Tuple of (n + 1),W st (a,x) . W = p & (a,v) . W = b & *' (a,p) = b holds
Phi x = v
let x be Tuple of (n + 1),W; :: thesis: ( (a,x) . W = p & (a,v) . W = b & *' (a,p) = b implies Phi x = v )
assume ( (a,x) . W = p & (a,v) . W = b & *' (a,p) = b ) ; :: thesis: Phi x = v
then Phi (a,x) = v by MIDSP_2:33;
hence Phi x = v by Def15; :: thesis: verum