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

consider a being 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 = (a,(0. W)) . W;
let x be Tuple of (n + 1),W; :: thesis: Phi (x +* (m,(0. W))) = 0. W
set p9 = ((a,x) . W) +* (m,a);
A2: (a,(0. W)) . W = a by MIDSP_2:40;
then A3: (a,(x +* (m,(0. W)))) . W = ((a,x) . W) +* (m,a) by Th29;
*' (a,(((a,x) . W) +* (m,a))) = (a,(0. W)) . W by A1, A2, Def6;
hence Phi (x +* (m,(0. W))) = 0. W by A3, Th27; :: 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: RAS has_property_of_zero_in m
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:39;
then ( W . (a,(p +* (m,a))) = (W . (a,p)) +* (m,(0. W)) & Phi ((W . (a,p)) +* (m,(0. W))) = W . (a,a) ) by A4, Th28;
hence *' (a,(p +* (m,a))) = a by Th26; :: thesis: verum

end;

hence RAS has_property_of_zero_in m by Def6; :: thesis: verum

end;