let x, y be object ; :: thesis: for p, q being XFinSequence st <%x%> ^ p = <%y%> ^ q holds
( x = y & p = q )
let p, q be XFinSequence; :: thesis: ( <%x%> ^ p = <%y%> ^ q implies ( x = y & p = q ) )
assume A1: <%x%> ^ p = <%y%> ^ q ; :: thesis: ( x = y & p = q )
(<%x%> ^ p) . 0 = x by Th32;
then x = y by A1, Th32;
hence ( x = y & p = q ) by A1, Th26; :: thesis: verum