let n be Element of NAT ; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr of n + 2
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . a,p = x iff a,x . W = p )
let RAS be non empty MidSp-like ReperAlgebraStr of n + 2; :: thesis: for a being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . a,p = x iff a,x . W = p )
let a be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . a,p = x iff a,x . W = p )
let p be Tuple of (n + 1),RAS; :: thesis: for W being ATLAS of RAS
for x being Tuple of (n + 1),W holds
( W . a,p = x iff a,x . W = p )
let W be ATLAS of RAS; :: thesis: for x being Tuple of (n + 1),W holds
( W . a,p = x iff a,x . W = p )
let x be Tuple of (n + 1),W; :: thesis: ( W . a,p = x iff a,x . W = p )
thus ( W . a,p = x implies a,x . W = p ) :: thesis: ( a,x . W = p implies W . a,p = x )

proof

assume A1: W . a,p = x ; :: thesis: a,x . W = p

now

let m be Nat of n; :: thesis: a,(x . m) . W = p . m
W . a,(p . m) = x . m by A1, Def12;
hence a,(x . m) . W = p . m by MIDSP_2:39; :: thesis: verum

end;

hence a,x . W = p by Def11; :: thesis: verum

end;

thus ( a,x . W = p implies W . a,p = x ) :: thesis: verum

proof

assume A2: a,x . W = p ; :: thesis: W . a,p = x

now

let m be Nat of n; :: thesis: W . a,(p . m) = x . m
a,(x . m) . W = p . m by A2, Def11;
hence W . a,(p . m) = x . m by MIDSP_2:39; :: thesis: verum

end;

hence W . a,p = x by Def12; :: thesis: verum

end;