let F be Element of Funcs ((REAL *),(REAL *)); :: thesis: for f being Element of REAL *
for n, i being Element of NAT holds ((repeat F) . 0) . f = f
let f be Element of REAL * ; :: thesis: for n, i being Element of NAT holds ((repeat F) . 0) . f = f
let n, i be Element of NAT ; :: thesis: ((repeat F) . 0) . f = f
thus ((repeat F) . 0) . f = (id (REAL *)) . f by Def2
.= f ; :: thesis: verum