theorem Th17: :: HILBERT2:17

for p, q being Element of HP-WFF
for t being FinSequence st p = q ^ t holds
p = q