let n be Nat; :: thesis: for m being Nat of n

for RAS being ReperAlgebra of n

for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

let W be ATLAS of RAS; :: thesis: ( m <= n implies ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) )

assume A1: m <= n ; :: thesis: ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

thus ( RAS is_alternative_in m implies for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) :: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) implies RAS is_alternative_in m )

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for pm being Point of RAS st p . m = pm holds

*' (a,(p +* ((m + 1),pm))) = a

for RAS being ReperAlgebra of n

for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS st m <= n holds

( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

let W be ATLAS of RAS; :: thesis: ( m <= n implies ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) )

assume A1: m <= n ; :: thesis: ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )

thus ( RAS is_alternative_in m implies for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) :: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) implies RAS is_alternative_in m )

proof

assume A4:
for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W
; :: thesis: RAS is_alternative_in m
set a = the Point of RAS;

assume A2: RAS is_alternative_in m ; :: thesis: for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W

let x be Tuple of (n + 1),W; :: thesis: Phi (x +* ((m + 1),(x . m))) = 0. W

set p = ( the Point of RAS,x) . W;

set b = ( the Point of RAS,(0. W)) . W;

set p9 = (( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m));

( the Point of RAS,(0. W)) . W = the Point of RAS by MIDSP_2:34;

then A3: *' ( the Point of RAS,((( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m)))) = ( the Point of RAS,(0. W)) . W by A2;

( the Point of RAS,(x +* ((m + 1),(x . m)))) . W = (( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m)) by A1, Th32;

hence Phi (x +* ((m + 1),(x . m))) = 0. W by A3, Th24; :: thesis: verum

end;assume A2: RAS is_alternative_in m ; :: thesis: for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W

let x be Tuple of (n + 1),W; :: thesis: Phi (x +* ((m + 1),(x . m))) = 0. W

set p = ( the Point of RAS,x) . W;

set b = ( the Point of RAS,(0. W)) . W;

set p9 = (( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m));

( the Point of RAS,(0. W)) . W = the Point of RAS by MIDSP_2:34;

then A3: *' ( the Point of RAS,((( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m)))) = ( the Point of RAS,(0. W)) . W by A2;

( the Point of RAS,(x +* ((m + 1),(x . m)))) . W = (( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m)) by A1, Th32;

hence Phi (x +* ((m + 1),(x . m))) = 0. W by A3, Th24; :: thesis: verum

for a being Point of RAS

for p being Tuple of (n + 1),RAS

for pm being Point of RAS st p . m = pm holds

*' (a,(p +* ((m + 1),pm))) = a

proof

hence
RAS is_alternative_in m
; :: thesis: verum
let a be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS

for pm being Point of RAS st p . m = pm holds

*' (a,(p +* ((m + 1),pm))) = a

let p be Tuple of (n + 1),RAS; :: thesis: for pm being Point of RAS st p . m = pm holds

*' (a,(p +* ((m + 1),pm))) = a

let pm be Point of RAS; :: thesis: ( p . m = pm implies *' (a,(p +* ((m + 1),pm))) = a )

assume A5: p . m = pm ; :: thesis: *' (a,(p +* ((m + 1),pm))) = a

set x = W . (a,p);

set v = W . (a,a);

set x9 = (W . (a,p)) +* ((m + 1),((W . (a,p)) . m));

W . (a,a) = 0. W by MIDSP_2:33;

then A6: Phi ((W . (a,p)) +* ((m + 1),((W . (a,p)) . m))) = W . (a,a) by A4;

W . (a,(p +* ((m + 1),(p . m)))) = (W . (a,p)) +* ((m + 1),((W . (a,p)) . m)) by A1, Th31;

hence *' (a,(p +* ((m + 1),pm))) = a by A5, A6, Th23; :: thesis: verum

end;for pm being Point of RAS st p . m = pm holds

*' (a,(p +* ((m + 1),pm))) = a

let p be Tuple of (n + 1),RAS; :: thesis: for pm being Point of RAS st p . m = pm holds

*' (a,(p +* ((m + 1),pm))) = a

let pm be Point of RAS; :: thesis: ( p . m = pm implies *' (a,(p +* ((m + 1),pm))) = a )

assume A5: p . m = pm ; :: thesis: *' (a,(p +* ((m + 1),pm))) = a

set x = W . (a,p);

set v = W . (a,a);

set x9 = (W . (a,p)) +* ((m + 1),((W . (a,p)) . m));

W . (a,a) = 0. W by MIDSP_2:33;

then A6: Phi ((W . (a,p)) +* ((m + 1),((W . (a,p)) . m))) = W . (a,a) by A4;

W . (a,(p +* ((m + 1),(p . m)))) = (W . (a,p)) +* ((m + 1),((W . (a,p)) . m)) by A1, Th31;

hence *' (a,(p +* ((m + 1),pm))) = a by A5, A6, Th23; :: thesis: verum