let n be Nat; :: thesis: for L being non empty right_zeroed addLoopStr
for x, y being Element of L holds (seq (n,x)) + (seq (n,y)) = seq (n,(x + y))
let L be non empty right_zeroed addLoopStr ; :: thesis: for x, y being Element of L holds (seq (n,x)) + (seq (n,y)) = seq (n,(x + y))
let x, y be Element of L; :: thesis: (seq (n,x)) + (seq (n,y)) = seq (n,(x + y))
let a be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((seq (n,x)) + (seq (n,y))) . a = (seq (n,(x + y))) . a
A1: ((seq (n,x)) + (seq (n,y))) . a = ((seq (n,x)) . a) + ((seq (n,y)) . a) by NORMSP_1:def 2;

per cases ( a = n or a <> n ) ;

suppose a = n ; :: thesis: ((seq (n,x)) + (seq (n,y))) . a = (seq (n,(x + y))) . a

then ( (seq (n,x)) . a = x & (seq (n,y)) . a = y & (seq (n,(x + y))) . a = x + y ) by Th24;
hence ((seq (n,x)) + (seq (n,y))) . a = (seq (n,(x + y))) . a by NORMSP_1:def 2; :: thesis: verum

end;

suppose a <> n ; :: thesis: ((seq (n,x)) + (seq (n,y))) . a = (seq (n,(x + y))) . a

then ( (seq (n,x)) . a = 0. L & (seq (n,y)) . a = 0. L & (seq (n,(x + y))) . a = 0. L ) by Th25;
hence ((seq (n,x)) + (seq (n,y))) . a = (seq (n,(x + y))) . a by A1, RLVECT_1:def 4; :: thesis: verum

end;

end;