let p be Element of REAL 3; :: thesis: ( len p = 3 & dom p = Seg 3 )
p = |[(p . 1),(p . 2),(p . 3)]| by Th1;
hence ( len p = 3 & dom p = Seg 3 ) by FINSEQ_1:45, FINSEQ_1:89; :: thesis: verum