let u be Element of (TOP-REAL 3); :: thesis: u = |[(u . 1),(u . 2),(u . 3)]|
thus u = |[(u `1),(u `2),(u `3)]| by EUCLID_5:3
.= |[(u . 1),(u `2),(u `3)]| by EUCLID_5:def 1
.= |[(u . 1),(u . 2),(u `3)]| by EUCLID_5:def 2
.= |[(u . 1),(u . 2),(u . 3)]| by EUCLID_5:def 3 ; :: thesis: verum