let z be object ; :: thesis: ( z in REAL implies ex u being object st
( u in REAL 3 & z = (proj (3,3)) . u ) )
assume z in REAL ; :: thesis: ex u being object st
( u in REAL 3 & z = (proj (3,3)) . u )
then reconsider z1 = z as Element of REAL ;
set x = the Element of REAL ;
reconsider u = <* the Element of REAL , the Element of REAL ,z1*> as Element of REAL 3 by FINSEQ_2:104;
(proj (3,3)) . u = u . 3 by PDIFF_1:def 1;
then (proj (3,3)) . u = z by FINSEQ_1:45;
hence ex u being object st
( u in REAL 3 & z = (proj (3,3)) . u ) ; :: thesis: verum

let x, y, z be Real; :: thesis: (proj (3,3)) . <*x,y,z*> = z
reconsider xx = x, yy = y, zz = z as Element of REAL by XREAL_0:def 1;
<*xx,yy,zz*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
then (proj (3,3)) . <*x,y,z*> = <*x,y,z*> . 3 by PDIFF_1:def 1;
hence (proj (3,3)) . <*x,y,z*> = z by FINSEQ_1:45; :: thesis: verum