let a, b be Real; :: thesis: ( |[a,b]| . 1 = a & |[a,b]| . 2 = b )
thus |[a,b]| . 1 = ((1,2) --> (a,b)) . 1 by Th4
.= a by FUNCT_4:63 ; :: thesis: |[a,b]| . 2 = b
thus |[a,b]| . 2 = ((1,2) --> (a,b)) . 2 by Th4
.= b by FUNCT_4:63 ; :: thesis: verum