let r, s be real number ; :: thesis: ( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )
thus proj2 . |[r,s]| = |[r,s]| `2 by Def29
.= s by EUCLID:56 ; :: thesis: proj1 . |[r,s]| = r
thus proj1 . |[r,s]| = |[r,s]| `1 by Def28
.= r by EUCLID:56 ; :: thesis: verum