hereby :: thesis: for x being Element of REAL holds
( (proj 1,1) . <*x*> = x & ((proj 1,1) " ) . x = <*x*> )

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 )
hence dom (proj i,n) = REAL n by Lema1, FUNCT_2:def 1, FUNCT_2:def 3, Lm1; :: thesis: rng (proj i,n) = REAL
proj i,n is onto by A1, Lema1;
hence rng (proj i,n) = REAL by A1, Lema1, FUNCT_2:def 1, FUNCT_2:def 3, Lm1; :: thesis: verum

end;

hence for x being Element of REAL holds
( (proj 1,1) . <*x*> = x & ((proj 1,1) " ) . x = <*x*> ) by Lm1, FUNCT_2:def 1, FUNCT_2:def 3, Lema1; :: thesis: verum