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

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

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

let W be ATLAS of RAS; :: thesis: ( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W )
thus ( RAS has_property_of_zero_in m implies for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ) :: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ) implies RAS has_property_of_zero_in m )
proof
set a = the Point of RAS;
assume A1: RAS has_property_of_zero_in m ; :: thesis: for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W
set b = ( the Point of RAS,(0. W)) . W;
let x be Tuple of (n + 1),W; :: thesis: Phi (x +* (m,(0. W))) = 0. W
set p9 = (( the Point of RAS,x) . W) +* (m, the Point of RAS);
A2: ( the Point of RAS,(0. W)) . W = the Point of RAS by MIDSP_2:34;
then A3: ( the Point of RAS,(x +* (m,(0. W)))) . W = (( the Point of RAS,x) . W) +* (m, the Point of RAS) by Th26;
*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m, the Point of RAS))) = ( the Point of RAS,(0. W)) . W by A1, A2;
hence Phi (x +* (m,(0. W))) = 0. W by ; :: thesis: verum
end;
thus ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ) implies RAS has_property_of_zero_in m ) :: thesis: verum
proof
assume A4: for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W ; :: thesis:
for a being Point of RAS
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (m,a))) = a
proof
let a be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS holds *' (a,(p +* (m,a))) = a
let p be Tuple of (n + 1),RAS; :: thesis: *' (a,(p +* (m,a))) = a
set v = W . (a,a);
set x9 = (W . (a,p)) +* (m,(0. W));
W . (a,a) = 0. W by MIDSP_2:33;
then ( W . (a,(p +* (m,a))) = (W . (a,p)) +* (m,(0. W)) & Phi ((W . (a,p)) +* (m,(0. W))) = W . (a,a) ) by ;
hence *' (a,(p +* (m,a))) = a by Th23; :: thesis: verum
end;
hence RAS has_property_of_zero_in m ; :: thesis: verum
end;