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 )
Y: n in NAT by ORDINAL1:def 13;
assume n > 0 ; :: thesis: (a followed_by b) . n = b
hence (a followed_by b) . n = (NAT --> b) . n by Th34
.= b by Y, FUNCOP_1:13 ;
:: thesis: verum