let n be Nat; :: thesis: for m being Nat of n

for RAS being ReperAlgebra of n

for W being ATLAS of RAS st RAS has_property_of_zero_in m holds

( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for W being ATLAS of RAS st RAS has_property_of_zero_in m holds

( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS st RAS has_property_of_zero_in m holds

( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

let W be ATLAS of RAS; :: thesis: ( RAS has_property_of_zero_in m implies ( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) )

assume A1: RAS has_property_of_zero_in m ; :: thesis: ( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

thus ( RAS is_additive_in m implies for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) :: thesis: ( ( for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m )

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m ) :: thesis: verum

for RAS being ReperAlgebra of n

for W being ATLAS of RAS st RAS has_property_of_zero_in m holds

( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n

for W being ATLAS of RAS st RAS has_property_of_zero_in m holds

( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS st RAS has_property_of_zero_in m holds

( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

let W be ATLAS of RAS; :: thesis: ( RAS has_property_of_zero_in m implies ( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) )

assume A1: RAS has_property_of_zero_in m ; :: thesis: ( RAS is_additive_in m iff for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) )

thus ( RAS is_additive_in m implies for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) :: thesis: ( ( for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m )

proof

thus
( ( for x being Tuple of (n + 1),W
set a = the Point of RAS;

assume A2: RAS is_additive_in m ; :: thesis: for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))

let x be Tuple of (n + 1),W; :: thesis: for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))

let v be Vector of W; :: thesis: Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))

set p = ( the Point of RAS,x) . W;

set p9m = ( the Point of RAS,v) . W;

consider p99m being Point of RAS such that

A3: p99m @ the Point of RAS = ((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W) by MIDSP_1:def 3;

A4: ( W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x & W . ( the Point of RAS,(( the Point of RAS,v) . W)) = v ) by Th15, MIDSP_2:33;

A5: W . ( the Point of RAS,p99m) = (W . ( the Point of RAS,((( the Point of RAS,x) . W) . m))) + (W . ( the Point of RAS,(( the Point of RAS,v) . W))) by A3, MIDSP_2:30

.= (x . m) + v by A4, Def9 ;

(( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W

A9: (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W

then A12: W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m))))) = (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) + (W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))))) by A3, Lm6;

Phi x = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W)))) by Lm5;

hence Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) by A12, A8, A9, Lm5; :: thesis: verum

end;assume A2: RAS is_additive_in m ; :: thesis: for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))

let x be Tuple of (n + 1),W; :: thesis: for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))

let v be Vector of W; :: thesis: Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v)))

set p = ( the Point of RAS,x) . W;

set p9m = ( the Point of RAS,v) . W;

consider p99m being Point of RAS such that

A3: p99m @ the Point of RAS = ((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W) by MIDSP_1:def 3;

A4: ( W . ( the Point of RAS,(( the Point of RAS,x) . W)) = x & W . ( the Point of RAS,(( the Point of RAS,v) . W)) = v ) by Th15, MIDSP_2:33;

A5: W . ( the Point of RAS,p99m) = (W . ( the Point of RAS,((( the Point of RAS,x) . W) . m))) + (W . ( the Point of RAS,(( the Point of RAS,v) . W))) by A3, MIDSP_2:30

.= (x . m) + v by A4, Def9 ;

(( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W

proof

then A8:
Phi (x +* (m,((x . m) + v))) = W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m)))))
by Lm5;
set pp = (( the Point of RAS,x) . W) +* (m,p99m);

set xx = x +* (m,((x . m) + v));

set qq = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W;

for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

end;set xx = x +* (m,((x . m) + v));

set qq = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W;

for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

proof

hence
(( the Point of RAS,x) . W) +* (m,p99m) = ( the Point of RAS,(x +* (m,((x . m) + v)))) . W
by Th9; :: thesis: verum
let i be Nat of n; :: thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

end;per cases
( i = m or i <> m )
;

end;

suppose A6:
i = m
; :: thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,p99m)) . i =
p99m
by Th10

.= ( the Point of RAS,((x . m) + v)) . W by A5, MIDSP_2:33

.= ( the Point of RAS,((x +* (m,((x . m) + v))) . m)) . W by Th13

.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by A6, Def8 ;

:: thesis: verum

end;.= ( the Point of RAS,((x . m) + v)) . W by A5, MIDSP_2:33

.= ( the Point of RAS,((x +* (m,((x . m) + v))) . m)) . W by Th13

.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by A6, Def8 ;

:: thesis: verum

suppose A7:
i <> m
; :: thesis: ((( the Point of RAS,x) . W) +* (m,p99m)) . i = (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,p99m)) . i =
(( the Point of RAS,x) . W) . i
by FUNCT_7:32

.= ( the Point of RAS,(x . i)) . W by Def8

.= ( the Point of RAS,((x +* (m,((x . m) + v))) . i)) . W by A7, FUNCT_7:32

.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by Def8 ;

:: thesis: verum

end;.= ( the Point of RAS,(x . i)) . W by Def8

.= ( the Point of RAS,((x +* (m,((x . m) + v))) . i)) . W by A7, FUNCT_7:32

.= (( the Point of RAS,(x +* (m,((x . m) + v)))) . W) . i by Def8 ;

:: thesis: verum

A9: (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W

proof

( RAS is_semi_additive_in m & *' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(((( the Point of RAS,x) . W) . m) @ (( the Point of RAS,v) . W))))) = (*' ( the Point of RAS,(( the Point of RAS,x) . W))) @ (*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))) )
by A1, A2, Th29;
set pp = (( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W));

set qq = ( the Point of RAS,(x +* (m,v))) . W;

for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

end;set qq = ( the Point of RAS,(x +* (m,v))) . W;

for i being Nat of n holds ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

proof

hence
(( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W)) = ( the Point of RAS,(x +* (m,v))) . W
by Th9; :: thesis: verum
let i be Nat of n; :: thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

end;per cases
( i = m or i <> m )
;

end;

suppose A10:
i = m
; :: thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i =
( the Point of RAS,v) . W
by Th10

.= ( the Point of RAS,((x +* (m,v)) . m)) . W by Th13

.= (( the Point of RAS,(x +* (m,v))) . W) . i by A10, Def8 ;

:: thesis: verum

end;.= ( the Point of RAS,((x +* (m,v)) . m)) . W by Th13

.= (( the Point of RAS,(x +* (m,v))) . W) . i by A10, Def8 ;

:: thesis: verum

suppose A11:
i <> m
; :: thesis: ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i = (( the Point of RAS,(x +* (m,v))) . W) . i

hence ((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))) . i =
(( the Point of RAS,x) . W) . i
by FUNCT_7:32

.= ( the Point of RAS,(x . i)) . W by Def8

.= ( the Point of RAS,((x +* (m,v)) . i)) . W by A11, FUNCT_7:32

.= (( the Point of RAS,(x +* (m,v))) . W) . i by Def8 ;

:: thesis: verum

end;.= ( the Point of RAS,(x . i)) . W by Def8

.= ( the Point of RAS,((x +* (m,v)) . i)) . W by A11, FUNCT_7:32

.= (( the Point of RAS,(x +* (m,v))) . W) . i by Def8 ;

:: thesis: verum

then A12: W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,p99m))))) = (W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W))))) + (W . ( the Point of RAS,(*' ( the Point of RAS,((( the Point of RAS,x) . W) +* (m,(( the Point of RAS,v) . W))))))) by A3, Lm6;

Phi x = W . ( the Point of RAS,(*' ( the Point of RAS,(( the Point of RAS,x) . W)))) by Lm5;

hence Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) by A12, A8, A9, Lm5; :: thesis: verum

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ) implies RAS is_additive_in m ) :: thesis: verum

proof

assume A13:
for x being Tuple of (n + 1),W

for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ; :: thesis: RAS is_additive_in m

then A14: RAS is_semi_additive_in m by Lm7;

for a, pm, p9m being Point of RAS

for p being Tuple of (n + 1),RAS st p . m = pm holds

*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

end;for v being Vector of W holds Phi (x +* (m,((x . m) + v))) = (Phi x) + (Phi (x +* (m,v))) ; :: thesis: RAS is_additive_in m

then A14: RAS is_semi_additive_in m by Lm7;

for a, pm, p9m being Point of RAS

for p being Tuple of (n + 1),RAS st p . m = pm holds

*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

proof

hence
RAS is_additive_in m
; :: thesis: verum
let a, pm, p9m be Point of RAS; :: thesis: for p being Tuple of (n + 1),RAS st p . m = pm holds

*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

let p be Tuple of (n + 1),RAS; :: thesis: ( p . m = pm implies *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) )

assume A15: p . m = pm ; :: thesis: *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

set x = W . (a,p);

set v = W . (a,p9m);

consider p99m being Point of RAS such that

A16: p99m @ a = (p . m) @ p9m by MIDSP_1:def 3;

A17: (a,(W . (a,p))) . W = p by Th15;

A18: W . (a,p99m) = (W . (a,(p . m))) + (W . (a,p9m)) by A16, MIDSP_2:30

.= ((W . (a,p)) . m) + (W . (a,p9m)) by Def9 ;

p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W

A22: (a,(W . (a,p9m))) . W = p9m by MIDSP_2:33;

p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W

Phi (W . (a,p)) = W . (a,(*' (a,p))) by Lm4;

then W . (a,(*' (a,(p +* (m,p99m))))) = (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m)))))) by A13, A21, A25;

hence *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) by A14, A15, A16, Lm6; :: thesis: verum

end;*' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

let p be Tuple of (n + 1),RAS; :: thesis: ( p . m = pm implies *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) )

assume A15: p . m = pm ; :: thesis: *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m))))

set x = W . (a,p);

set v = W . (a,p9m);

consider p99m being Point of RAS such that

A16: p99m @ a = (p . m) @ p9m by MIDSP_1:def 3;

A17: (a,(W . (a,p))) . W = p by Th15;

A18: W . (a,p99m) = (W . (a,(p . m))) + (W . (a,p9m)) by A16, MIDSP_2:30

.= ((W . (a,p)) . m) + (W . (a,p9m)) by Def9 ;

p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W

proof

then A21:
Phi ((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) = W . (a,(*' (a,(p +* (m,p99m)))))
by Lm5;
set pp = p +* (m,p99m);

set xx = (W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))));

set qq = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W;

for i being Nat of n holds (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

end;set xx = (W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))));

set qq = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W;

for i being Nat of n holds (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

proof

hence
p +* (m,p99m) = (a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W
by Th9; :: thesis: verum
let i be Nat of n; :: thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

end;per cases
( i = m or i <> m )
;

end;

suppose A19:
i = m
; :: thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

hence (p +* (m,p99m)) . i =
p99m
by Th10

.= (a,(((W . (a,p)) . m) + (W . (a,p9m)))) . W by A18, MIDSP_2:33

.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . m)) . W by Th13

.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by A19, Def8 ;

:: thesis: verum

end;.= (a,(((W . (a,p)) . m) + (W . (a,p9m)))) . W by A18, MIDSP_2:33

.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . m)) . W by Th13

.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by A19, Def8 ;

:: thesis: verum

suppose A20:
i <> m
; :: thesis: (p +* (m,p99m)) . i = ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i

hence (p +* (m,p99m)) . i =
p . i
by FUNCT_7:32

.= (a,((W . (a,p)) . i)) . W by A17, Def8

.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . i)) . W by A20, FUNCT_7:32

.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by Def8 ;

:: thesis: verum

end;.= (a,((W . (a,p)) . i)) . W by A17, Def8

.= (a,(((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m))))) . i)) . W by A20, FUNCT_7:32

.= ((a,((W . (a,p)) +* (m,(((W . (a,p)) . m) + (W . (a,p9m)))))) . W) . i by Def8 ;

:: thesis: verum

A22: (a,(W . (a,p9m))) . W = p9m by MIDSP_2:33;

p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W

proof

then A25:
Phi ((W . (a,p)) +* (m,(W . (a,p9m)))) = W . (a,(*' (a,(p +* (m,p9m)))))
by Lm5;
set pp = p +* (m,p9m);

set qq = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W;

for i being Nat of n holds (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

end;set qq = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W;

for i being Nat of n holds (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

proof

hence
p +* (m,p9m) = (a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W
by Th9; :: thesis: verum
let i be Nat of n; :: thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

end;per cases
( i = m or i <> m )
;

end;

suppose A23:
i = m
; :: thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

hence (p +* (m,p9m)) . i =
p9m
by Th10

.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . m)) . W by A22, Th13

.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by A23, Def8 ;

:: thesis: verum

end;.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . m)) . W by A22, Th13

.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by A23, Def8 ;

:: thesis: verum

suppose A24:
i <> m
; :: thesis: (p +* (m,p9m)) . i = ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i

hence (p +* (m,p9m)) . i =
p . i
by FUNCT_7:32

.= (a,((W . (a,p)) . i)) . W by A17, Def8

.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . i)) . W by A24, FUNCT_7:32

.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by Def8 ;

:: thesis: verum

end;.= (a,((W . (a,p)) . i)) . W by A17, Def8

.= (a,(((W . (a,p)) +* (m,(W . (a,p9m)))) . i)) . W by A24, FUNCT_7:32

.= ((a,((W . (a,p)) +* (m,(W . (a,p9m))))) . W) . i by Def8 ;

:: thesis: verum

Phi (W . (a,p)) = W . (a,(*' (a,p))) by Lm4;

then W . (a,(*' (a,(p +* (m,p99m))))) = (W . (a,(*' (a,p)))) + (W . (a,(*' (a,(p +* (m,p9m)))))) by A13, A21, A25;

hence *' (a,(p +* (m,(pm @ p9m)))) = (*' (a,p)) @ (*' (a,(p +* (m,p9m)))) by A14, A15, A16, Lm6; :: thesis: verum