let f be Function; :: thesis: for i, j being object st i in dom f & j in dom f holds
f = f +* ((i,j) --> ((f . i),(f . j)))
let i, j be object ; :: thesis: ( i in dom f & j in dom f implies f = f +* ((i,j) --> ((f . i),(f . j))) )
assume A1: ( i in dom f & j in dom f ) ; :: thesis: f = f +* ((i,j) --> ((f . i),(f . j)))
thus f = f +* (j .--> (f . j)) by A1, FUNCT_4:7, LATTICE2:5
.= (f +* (i .--> (f . i))) +* (j .--> (f . j)) by A1, FUNCT_4:7, LATTICE2:5
.= f +* ((i .--> (f . i)) +* (j .--> (f . j))) by FUNCT_4:14
.= f +* ((i,j) --> ((f . i),(f . j))) by FUNCT_4:def 4 ; :: thesis: verum