let n be Nat; :: thesis: for L being non empty ZeroStr holds seq (n,(0. L)) = 0_. L
let L be non empty ZeroStr ; :: thesis: seq (n,(0. L)) = 0_. L
let m be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (seq (n,(0. L))) . m = (0_. L) . m

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

suppose m = n ; :: thesis: (seq (n,(0. L))) . m = (0_. L) . m

hence (seq (n,(0. L))) . m = 0. L by Th24
.= (0_. L) . m ;
:: thesis: verum

end;

suppose m <> n ; :: thesis: (seq (n,(0. L))) . m = (0_. L) . m

hence (seq (n,(0. L))) . m = (0_. L) . m by FUNCT_7:32; :: thesis: verum

end;

end;