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