let a be object ; :: thesis: 3 |-> a = <*a,a,a*>
thus 3 |-> a = (2 + 1) |-> a
.= (2 |-> a) ^ <*a*> by Th58
.= <*a,a*> ^ <*a*> by Th59
.= <*a,a,a*> ; :: thesis: verum