let a, b, c, d be Element of the carrier of the WeakAffVect; ( [[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
;
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;
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; verum