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;