let n be Element of 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 W . a,p = x 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 W . a,p = x 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 W . a,p = x 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 W . a,p = x holds
Phi x = W . a,(*' a,p)
let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W st W . a,p = x holds
Phi x = W . a,(*' a,p)
let x be Tuple of (n + 1),W; :: thesis: ( W . a,p = x implies Phi x = W . a,(*' a,p) )
assume A1: W . a,p = x ; :: thesis: Phi x = W . a,(*' a,p)
thus Phi x = Phi a,x by Def15
.= W . a,(*' a,p) by A1, Th17 ; :: thesis: verum