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
A7: ( dom g1 = REAL * & ( for h being Element of REAL * holds g1 . h = ((repeat f) . (LifeSpan f,h,n)) . h ) ) and
A8: ( dom g2 = REAL * & ( for h being Element of REAL * holds g2 . h = ((repeat f) . (LifeSpan f,h,n)) . h ) ) ; :: thesis: g1 = g2

now

let xx be set ; :: 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 A7;
thus g1 . xx = ((repeat f) . (LifeSpan f,h,n)) . h by A7
.= g2 . xx by A8 ; :: thesis: verum

end;

hence g1 = g2 by A7, A8, FUNCT_1:9; :: thesis: verum