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;

hence phi = (<*x*> ^ phi2) ^ p2 by A2; :: thesis: verum

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
( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi )
; :: thesis: phi = (<*x*> ^ phi2) ^ p2assume 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;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

hence phi = (<*x*> ^ phi2) ^ p2 by A2; :: thesis: verum