let x, y be set ; :: 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 AFINSQ_1:35;
then x = y by A1, AFINSQ_1:35;
hence ( x = y & p = q ) by A1, AFINSQ_1:28; :: thesis: verum