let n be Nat; :: thesis: for RAS being ReperAlgebra of n
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
let RAS be ReperAlgebra of n; :: thesis: for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
let a be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS
for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W st (a,x) . W = p holds
Phi x = W . (a,(*' (a,p)))
let x be Tuple of (n + 1),W; :: thesis: ( (a,x) . W = p implies Phi x = W . (a,(*' (a,p))) )
assume (a,x) . W = p ; :: thesis: Phi x = W . (a,(*' (a,p)))
then W . (a,p) = x by Th15;
hence Phi x = W . (a,(*' (a,p))) by Lm4; :: thesis: verum