let L be non empty multLoopStr_0 ; :: thesis: ( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
( not the carrier of L is empty & 0 in NAT ) ;
then 0 in dom (0_. L) by FUNCT_2:def 1;
hence (1_. L) . 0 = 1. L by FUNCT_7:33; :: thesis: for n being Nat st n <> 0 holds
(1_. L) . n = 0. L
let n be Nat; :: thesis: ( n <> 0 implies (1_. L) . n = 0. L )
A1: n in NAT by ORDINAL1:def 13;
assume n <> 0 ; :: thesis: (1_. L) . n = 0. L
hence (1_. L) . n = (0_. L) . n by FUNCT_7:34
.= 0. L by A1, FUNCOP_1:13 ;
:: thesis: verum