now

let i, n be Element of NAT ; :: thesis: ( i in Seg n implies ( dom (proj i,n) = REAL n & rng (proj i,n) = REAL ) )
assume A1: i in Seg n ; :: thesis: ( dom (proj i,n) = REAL n & rng (proj i,n) = REAL )
thus dom (proj i,n) = REAL n by FUNCT_2:def 1; :: thesis: rng (proj i,n) = REAL
proj i,n is onto by A1, Lm2;
hence rng (proj i,n) = REAL by FUNCT_2:def 3; :: thesis: verum

end;

hence ( ( for i, n being Element of NAT st i in Seg n holds
( dom (proj i,n) = REAL n & rng (proj i,n) = REAL ) ) & ( for x being Element of REAL holds
( (proj 1,1) . <*x*> = x & ((proj 1,1) " ) . x = <*x*> ) ) ) by Lm1; :: thesis: verum