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 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 Def12

.= W . (a,(*' (a,p))) by A1, Th15 ; :: thesis: verum

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 Def12

.= W . (a,(*' (a,p))) by A1, Th15 ; :: thesis: verum