let n be Element of NAT ; :: thesis: for RAS being ReperAlgebra of n
for a, b being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let RAS be ReperAlgebra of n; :: thesis: for a, b being Point of RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let a, b be Point of RAS; :: thesis: for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)
let x be Tuple of (n + 1),W; :: thesis: Phi (a,x) = Phi (b,x)
RAS is being_invariance by Def14;
hence Phi (a,x) = Phi (b,x) by Th21; :: thesis: verum