now :: thesis: for o being object st o in { (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } holds
o in the carrier of (R ^* n)

let o be object ; :: thesis: ( o in { (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } implies o in the carrier of (R ^* n) )
assume o in { (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } ; :: thesis: o in the carrier of (R ^* n)
then consider i being Nat such that
A: ( o = i _th_unit_vector (n,R) & 1 <= i & i <= n ) ;
the carrier of (R ^* n) = n -tuples_on the carrier of R by DEF;
hence o in the carrier of (R ^* n) by A; :: thesis: verum

end;

hence { (i _th_unit_vector (n,R)) where i is Nat : ( 1 <= i & i <= n ) } is Subset of (R ^* n) by TARSKI:def 3; :: thesis: verum