let a, b be object ; :: thesis: for p, q being FinSequence st p ^ <*a*> = q ^ <*b*> holds
( p = q & a = b )
let p, q be FinSequence; :: thesis: ( p ^ <*a*> = q ^ <*b*> implies ( p = q & a = b ) )
assume A1: p ^ <*a*> = q ^ <*b*> ; :: thesis: ( p = q & a = b )
A2: ( (p ^ <*a*>) . ((len p) + 1) = a & (q ^ <*b*>) . ((len q) + 1) = b ) by FINSEQ_1:42;
( len (p ^ <*a*>) = (len p) + 1 & len (q ^ <*b*>) = (len q) + 1 ) by Th14;
hence ( p = q & a = b ) by A1, A2, FINSEQ_1:33; :: thesis: verum