now :: thesis: for i, n being Nat st i in Seg n holds

( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL )

hence
( ( 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;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

( 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