let n be Element of NAT ; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr of 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 of 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 A1: ( W . a,p = x & W . a,b = v ) ; :: thesis: ( *' a,p = b iff Phi a,x = v )
then Phi a,x = W . a,(*' a,p) by Th17;
hence ( *' a,p = b iff Phi a,x = v ) by A1, MIDSP_2:38; :: thesis: verum