now :: thesis: for i, n being Nat st i in Seg n holds
( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL )

let i, n be 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 Nat st i in Seg n holds
( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by Lm1; :: thesis: verum