set f = proj (3,3);
A1:
for z being object st z in REAL holds
ex u being object st
( u in REAL 3 & z = (proj (3,3)) . u )
now for x, y, z being Real holds (proj (3,3)) . <*x,y,z*> = zlet x,
y,
z be
Real;
(proj (3,3)) . <*x,y,z*> = zreconsider 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;
verum end;
hence
( dom (proj (3,3)) = REAL 3 & rng (proj (3,3)) = REAL & ( for x, y, z being Real holds (proj (3,3)) . <*x,y,z*> = z ) )
by A1, FUNCT_2:10, FUNCT_2:def 1; verum