let f be Function; :: thesis: for i, x being set holds f = (f +* (i,x)) +* (i,(f . i))
let i, x be set ; :: thesis: f = (f +* (i,x)) +* (i,(f . i))
thus f = f +* (i,(f . i)) by FUNCT_7:35
.= (f +* (i,x)) +* (i,(f . i)) by FUNCT_7:34 ; :: thesis: verum