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