let m, n be Nat; :: thesis: for L being non empty ZeroStr
for x being Element of L st m <> n holds
(seq (n,x)) . m = 0. L
let L be non empty ZeroStr ; :: thesis: for x being Element of L st m <> n holds
(seq (n,x)) . m = 0. L
let x be Element of L; :: thesis: ( m <> n implies (seq (n,x)) . m = 0. L )
assume m <> n ; :: thesis: (seq (n,x)) . m = 0. L
hence (seq (n,x)) . m = (0_. L) . m by FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum