theorem Th23: :: FOMODEL2:23

for x being set
for S being Language
for p2 being FinSequence
for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) )