let n be Element of 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 Def15;
hence *' a,p = b by A1, Th20; :: thesis: verum