let a, b, c, d be Element of the carrier of the WeakAffVect; :: thesis: ( [[a,b],[c,d]] in P iff a,b '||' c,d )
A1: ( [[a,b],[c,d]] in P implies a,b '||' c,d )

proof

assume [[a,b],[c,d]] in P ; :: thesis: a,b '||' c,d
then consider a9, b9, c9, d9 being Element of the carrier of the WeakAffVect such that
A2: [a,b] = [a9,b9] and
A3: [c,d] = [c9,d9] and
A4: a9,b9 '||' c9,d9 by Lm13;
A5: c = c9 by A3, XTUPLE_0:1;
( a = a9 & b = b9 ) by A2, XTUPLE_0:1;
hence a,b '||' c,d by A3, A4, A5, XTUPLE_0:1; :: thesis: verum

end;

( [a,b] in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] & [c,d] in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] ) by ZFMISC_1:def 2;
hence ( [[a,b],[c,d]] in P iff a,b '||' c,d ) by A1, Lm13; :: thesis: verum