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