let n be Element of 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 )

proof

consider a being 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 = (a,x) . W;
set b = (a,(0. W)) . W;
set p9 = ((a,x) . W) +* ((m + 1),(((a,x) . W) . m));
(a,(0. W)) . W = a by MIDSP_2:40;
then A3: *' (a,(((a,x) . W) +* ((m + 1),(((a,x) . W) . m)))) = (a,(0. W)) . W by A2, Def9;
(a,(x +* ((m + 1),(x . m)))) . W = ((a,x) . W) +* ((m + 1),(((a,x) . W) . m)) by A1, Th35;
hence Phi (x +* ((m + 1),(x . m))) = 0. W by A3, Th27; :: thesis: verum

end;

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

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
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

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:39;
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, Th34;
hence *' (a,(p +* ((m + 1),pm))) = a by A5, A6, Th26; :: thesis: verum

end;

hence RAS is_alternative_in m by Def9; :: thesis: verum

end;