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 )

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

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

end;now :: thesis: for m being Nat of n holds (a,(x . m)) . W = p . m

hence
(a,x) . W = p
by Def8; :: thesis: verumlet 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;W . (a,(p . m)) = x . m by A1, Def9;

hence (a,(x . m)) . W = p . m by MIDSP_2:33; :: thesis: verum

proof

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

end;now :: thesis: for m being Nat of n holds W . (a,(p . m)) = x . m

hence
W . (a,p) = x
by Def9; :: thesis: verumlet 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;(a,(x . m)) . W = p . m by A2, Def8;

hence W . (a,(p . m)) = x . m by MIDSP_2:33; :: thesis: verum