let a, b be set ; :: thesis: for n being Nat st n > 0 holds
(a followed_by b) . n = b
let n be Nat; :: thesis: ( n > 0 implies (a followed_by b) . n = b )
A1: n in NAT by ORDINAL1:def 12;
assume n > 0 ; :: thesis: (a followed_by b) . n = b
hence (a followed_by b) . n = (NAT --> b) . n by Th31
.= b by A1, FUNCOP_1:7 ;
:: thesis: verum