let a, b, c, d be Element of the carrier of AFV0; :: 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 a', b', c', d' being Element of the carrier of AFV0 such that
A2: ( [a,b] = [a',b'] & [c,d] = [c',d'] ) and
A3: a',b' '||' c',d' by Lm13;
( a = a' & b = b' & c = c' & d = d' ) by A2, ZFMISC_1:33;
hence a,b '||' c,d by A3; :: thesis: verum

end;

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