let n be Nat; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr over n + 2

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: 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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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

( *' (a,p) = b iff Phi (a,x) = v )

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

assume that

A1: W . (a,p) = x and

A2: W . (a,b) = v ; :: thesis: ( *' (a,p) = b iff Phi (a,x) = v )

Phi (a,x) = W . (a,(*' (a,p))) by A1, Th15;

hence ( *' (a,p) = b iff Phi (a,x) = v ) by A2, MIDSP_2:32; :: 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 holds

( *' (a,p) = b iff Phi (a,x) = v )

let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; :: 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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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 holds

( *' (a,p) = b iff Phi (a,x) = v )

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

( *' (a,p) = b iff Phi (a,x) = v )

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

assume that

A1: W . (a,p) = x and

A2: W . (a,b) = v ; :: thesis: ( *' (a,p) = b iff Phi (a,x) = v )

Phi (a,x) = W . (a,(*' (a,p))) by A1, Th15;

hence ( *' (a,p) = b iff Phi (a,x) = v ) by A2, MIDSP_2:32; :: thesis: verum