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

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

hence
g1 = g2
by A6, A8, FUNCT_1:2; :: thesis: verumg1 . 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;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