let p1, p2, q be FinSequence; :: thesis: ( p1 c= q & p2 c= q & len p1 = len p2 implies p1 = p2 )
assume that
A1: p1 c= q and
A2: p2 c= q and
A3: len p1 = len p2 ; :: thesis: p1 = p2
reconsider i = len p1 as Element of NAT ;
A4: ( dom p1 = Seg i & dom p2 = Seg i ) by A3, FINSEQ_1:def 3;

now :: thesis: for j being Nat st j in dom p1 holds
p1 . j = p2 . j

let j be Nat; :: thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A5: j in dom p1 ; :: thesis: p1 . j = p2 . j
hence p1 . j = q . j by A1, GRFUNC_1:2
.= p2 . j by A2, A4, A5, GRFUNC_1:2 ;
:: thesis: verum

end;

hence p1 = p2 by A4; :: thesis: verum