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;