let n be Nat; :: thesis: for L being non empty ZeroStr holds (0_. L) || n = 0_. L
let L be non empty ZeroStr ; :: thesis: (0_. L) || n = 0_. L
let m be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((0_. L) || n) . m = (0_. L) . m
( m = n or m <> n ) ;
hence ((0_. L) || n) . m = (0_. L) . m by Th32, FUNCT_7:32; :: thesis: verum