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;