let p, q, r, s be Element of HP-WFF ; :: thesis: ( p ^ q = r ^ s implies ( p = r & q = s ) )
assume A1: p ^ q = r ^ s ; :: thesis: ( p = r & q = s )

per cases ( len p <= len r or len p >= len r ) ;

suppose len p <= len r ; :: thesis: ( p = r & q = s )

then ex t being FinSequence st p ^ t = r by A1, FINSEQ_1:47;
hence p = r by Th17; :: thesis: q = s
hence q = s by A1, FINSEQ_1:33; :: thesis: verum

end;

suppose len p >= len r ; :: thesis: ( p = r & q = s )

then ex t being FinSequence st r ^ t = p by A1, FINSEQ_1:47;
hence p = r by Th17; :: thesis: q = s
hence q = s by A1, FINSEQ_1:33; :: thesis: verum

end;

end;