set X = REAL * ;
let g1, g2 be Element of Funcs ((REAL *),(REAL *)); :: thesis: ( dom g1 = REAL * & ( for h being Element of REAL * holds g1 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) & dom g2 = REAL * & ( for h being Element of REAL * holds g2 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) implies g1 = g2 )
assume that
A6: dom g1 = REAL * and
A7: for h being Element of REAL * holds g1 . h = ((repeat f) . (LifeSpan (f,h,n))) . h and
A8: dom g2 = REAL * and
A9: for h being Element of REAL * holds g2 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ; :: thesis: g1 = g2
now :: thesis: for xx being object st xx in dom g1 holds
g1 . xx = g2 . xx
let xx be object ; :: thesis: ( xx in dom g1 implies g1 . xx = g2 . xx )
assume xx in dom g1 ; :: thesis: g1 . xx = g2 . xx
then reconsider h = xx as Element of REAL * by A6;
thus g1 . xx = ((repeat f) . (LifeSpan (f,h,n))) . h by A7
.= g2 . xx by A9 ; :: thesis: verum
end;
hence g1 = g2 by A6, A8, FUNCT_1:2; :: thesis: verum