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