consider u being Vector of M such that
A1: for p being Element of [: the carrier of M, the carrier of M:] holds
( p in u iff p `1 = p `2 ) by Th31;
u = { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 }

proof

for x being object holds
( x in u iff x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } )

proof

let x be object ; :: thesis: ( x in u iff x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } )
thus ( x in u implies x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ) :: thesis: ( x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } implies x in u )

proof

assume A2: x in u ; :: thesis: x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 }
then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;
r `1 = r `2 by A1, A2;
hence x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ; :: thesis: verum

end;

thus ( x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } implies x in u ) :: thesis: verum

proof

assume x in { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ; :: thesis: x in u
then ex p being Element of [: the carrier of M, the carrier of M:] st
( x = p & p `1 = p `2 ) ;
hence x in u by A1; :: thesis: verum

end;

end;

hence u = { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } by TARSKI:2; :: thesis: verum

end;

hence { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } is Vector of M ; :: thesis: verum