let Al be QC-alphabet ; :: thesis:
let Al2 be Al -expanding QC-alphabet ; :: thesis:
let f be FinSequence of CQC-WFF Al2; :: thesis:
let g be FinSequence of CQC-WFF Al; :: thesis:
assume A1: f = g ; :: thesis:

suppose A2: len f > 0 ; :: thesis:

then consider k being Nat such that
A3: len f = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
thus Ant f = g | (Seg k) by A1, A2, A3, CALCUL_1:def 1
.= Ant g by A1, A2, A3, CALCUL_1:def 1 ; :: thesis:
Suc f = g . (len g) by A1, A2, CALCUL_1:def 2
.= Suc g by A1, A2, CALCUL_1:def 2 ;
hence Suc f = Suc g ; :: thesis:

end;

suppose A4: not len f > 0 ; :: thesis:

thus Ant f = {} by A4, CALCUL_1:def 1
.= Ant g by A1, A4, CALCUL_1:def 1 ; :: thesis:
thus Suc f = VERUM Al2 by A4, CALCUL_1:def 2
.= VERUM Al
.= Suc g by A1, A4, CALCUL_1:def 2 ; :: thesis:

end;

end;