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 )

hence ( [[a,b],[c,d]] in P iff a,b '||' c,d ) by A1, Lm13; :: thesis: verum

A1: ( [[a,b],[c,d]] in P implies a,b '||' c,d )

proof

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

hence ( [[a,b],[c,d]] in P iff a,b '||' c,d ) by A1, Lm13; :: thesis: verum