let x, t be Real; :: thesis: for z being Element of REAL 2 st z = <*x,t*> holds
( (proj (1,2)) . z = x & (proj (2,2)) . z = t )
let z be Element of REAL 2; :: thesis: ( z = <*x,t*> implies ( (proj (1,2)) . z = x & (proj (2,2)) . z = t ) )
assume AS: z = <*x,t*> ; :: thesis: ( (proj (1,2)) . z = x & (proj (2,2)) . z = t )
thus (proj (1,2)) . z = z . 1 by PDIFF_1:def 1
.= x by AS ; :: thesis: (proj (2,2)) . z = t
thus (proj (2,2)) . z = z . 2 by PDIFF_1:def 1
.= t by AS ; :: thesis: verum