let n be Nat; :: thesis: for RAS being ReperAlgebra of n

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let RAS be ReperAlgebra of n; :: thesis: for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let a, b be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let W be ATLAS of RAS; :: thesis: for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let v be Vector of W; :: thesis: for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let x be Tuple of (n + 1),W; :: thesis: ( W . (a,p) = x & W . (a,b) = v & Phi x = v implies *' (a,p) = b )

assume A1: ( W . (a,p) = x & W . (a,b) = v & Phi x = v ) ; :: thesis: *' (a,p) = b

Phi x = Phi (a,x) by Def12;

hence *' (a,p) = b by A1, Th18; :: thesis: verum

for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let RAS be ReperAlgebra of n; :: thesis: for a, b being Point of RAS

for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let a, b be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS

for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let W be ATLAS of RAS; :: thesis: for v being Vector of W

for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let v be Vector of W; :: thesis: for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v & Phi x = v holds

*' (a,p) = b

let x be Tuple of (n + 1),W; :: thesis: ( W . (a,p) = x & W . (a,b) = v & Phi x = v implies *' (a,p) = b )

assume A1: ( W . (a,p) = x & W . (a,b) = v & Phi x = v ) ; :: thesis: *' (a,p) = b

Phi x = Phi (a,x) by Def12;

hence *' (a,p) = b by A1, Th18; :: thesis: verum