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 }

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

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
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 } )

end;( 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

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
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 )

end;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

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
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;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