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

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