let n be Nat; 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; 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; 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; 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; 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; ( W . (a,p) = x implies Phi x = W . (a,(*' (a,p))) )
assume A1:
W . (a,p) = x
; Phi x = W . (a,(*' (a,p)))
thus Phi x =
Phi (a,x)
by Def12
.=
W . (a,(*' (a,p)))
by A1, Th15
; verum