let x be set ; :: thesis: 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 = () . phi & phi2 = head phi & p2 = tail phi ) )

let S be Language; :: thesis: for p2 being FinSequence
for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = () . phi & phi2 = head phi & p2 = tail phi ) )

let p2 be FinSequence; :: thesis: for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = () . phi & phi2 = head phi & p2 = tail phi ) )

let phi, phi2 be wff string of S; :: thesis: ( not phi is 0wff implies ( phi = (<*x*> ^ phi2) ^ p2 iff ( x = () . phi & phi2 = head phi & p2 = tail phi ) ) )
set Phi = SubWffsOf phi;
set F = S -firstChar ;
set s = () . phi;
set SS = AllSymbolsOf S;
assume A1: not phi is 0wff ; :: thesis: ( phi = (<*x*> ^ phi2) ^ p2 iff ( x = () . phi & phi2 = head phi & p2 = tail phi ) )
then consider phi1 being wff string of S, p being FinSequence such that
A2: ( p is AllSymbolsOf S -valued & SubWffsOf phi = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p ) by Def34;
hereby :: thesis: ( x = () . phi & phi2 = head phi & p2 = tail phi implies phi = (<*x*> ^ phi2) ^ p2 )
assume A4: phi = (<*x*> ^ phi2) ^ p2 ; :: thesis: ( x = () . phi & phi2 = head phi & p2 = tail phi )
then A5: phi . 1 = (<*x*> ^ (phi2 ^ p2)) . 1 by FINSEQ_1:32
.= x by FINSEQ_1:41 ;
hence x = () . phi by FOMODEL0:6; :: thesis: ( phi2 = head phi & p2 = tail phi )
( rng p2 c= rng phi & rng phi c= AllSymbolsOf S ) by ;
then ( p2 is AllSymbolsOf S -valued & [phi2,p2] = [phi2,p2] & phi = (<*(() . phi)*> ^ phi2) ^ p2 ) by ;
then SubWffsOf phi = [phi2,p2] by ;
hence ( phi2 = head phi & p2 = tail phi ) ; :: thesis: verum
end;
assume ( x = () . phi & phi2 = head phi & p2 = tail phi ) ; :: thesis: phi = (<*x*> ^ phi2) ^ p2
hence phi = (<*x*> ^ phi2) ^ p2 by A2; :: thesis: verum