let n be Nat; :: thesis: for RAS being non empty MidSp-like ReperAlgebraStr over 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 over 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 :: thesis: for m being Nat of n holds (a,(x . m)) . W = p . m

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

end;

hence (a,x) . W = p by Def8; :: 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 :: thesis: for m being Nat of n holds W . (a,(p . m)) = x . m

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

end;

hence W . (a,p) = x by Def9; :: thesis: verum

end;