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 )

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

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
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 A3, Th24; :: thesis: verum

end;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 A3, Th24; :: 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

end;for a being Point of RAS

for p being Tuple of (n + 1),RAS holds *' (a,(p +* (m,a))) = a

proof

hence
RAS has_property_of_zero_in m
; :: thesis: verum
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 A4, Th25;

hence *' (a,(p +* (m,a))) = a by Th23; :: thesis: verum

end;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 A4, Th25;

hence *' (a,(p +* (m,a))) = a by Th23; :: thesis: verum