let B be antichain; for p, q, r, s being FinSequence st p ^ q = r ^ s & p in B & r in B holds
( p = r & q = s )
let p, q, r, s be FinSequence; ( p ^ q = r ^ s & p in B & r in B implies ( p = r & q = s ) )
assume that
A2:
p ^ q = r ^ s
and
A3:
( p in B & r in B )
; ( p = r & q = s )
consider t being FinSequence such that
A4:
( p ^ t = r or p = r ^ t )
by TH1, A2;
thus
p = r
by A3, A4, Th1; q = s
hence
q = s
by A2, FINSEQ_1:33; verum