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 = (S -firstChar) . 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 = (S -firstChar) . 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 = (S -firstChar) . 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 = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) ) )
set Phi = SubWffsOf phi;
set F = S -firstChar ;
set s = (S -firstChar) . phi;
set SS = AllSymbolsOf S;
assume A1: not phi is 0wff ; :: thesis: ( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . 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 = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) by Def34;

hereby :: thesis: ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi implies phi = (<*x*> ^ phi2) ^ p2 )

assume A4: phi = (<*x*> ^ phi2) ^ p2 ; :: thesis: ( x = (S -firstChar) . 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 = (S -firstChar) . phi by FOMODEL0:6; :: thesis: ( phi2 = head phi & p2 = tail phi )
( rng p2 c= rng phi & rng phi c= AllSymbolsOf S ) by A4, FINSEQ_1:30, RELAT_1:def 19;
then ( p2 is AllSymbolsOf S -valued & [phi2,p2] = [phi2,p2] & phi = (<*((S -firstChar) . phi)*> ^ phi2) ^ p2 ) by XBOOLE_1:1, RELAT_1:def 19, A5, FOMODEL0:6, A4;
then SubWffsOf phi = [phi2,p2] by A1, Def34;
hence ( phi2 = head phi & p2 = tail phi ) ; :: thesis: verum

end;

assume ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) ; :: thesis: phi = (<*x*> ^ phi2) ^ p2
hence phi = (<*x*> ^ phi2) ^ p2 by A2; :: thesis: verum