let a, b be real number ; :: thesis: ( |[a,b]| . 1 = a & |[a,b]| . 2 = b )
thus |[a,b]| . 1 = (1,2 --> a,b) . 1 by Th25
.= a by FUNCT_4:66 ; :: thesis: |[a,b]| . 2 = b
thus |[a,b]| . 2 = (1,2 --> a,b) . 2 by Th25
.= b by FUNCT_4:66 ; :: thesis: verum