let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al holds

( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al holds

( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

let f be FinSequence of CQC-WFF Al; :: thesis: ( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

set fin = f ^ <*p*>;

A1: len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:16;

then (f ^ <*p*>) . (len (f ^ <*p*>)) = p by FINSEQ_1:42;

hence Suc (f ^ <*p*>) = p by Def2; :: thesis: Ant (f ^ <*p*>) = f

thus Ant (f ^ <*p*>) = f :: thesis: verum

for f being FinSequence of CQC-WFF Al holds

( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al holds

( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

let f be FinSequence of CQC-WFF Al; :: thesis: ( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f )

set fin = f ^ <*p*>;

A1: len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:16;

then (f ^ <*p*>) . (len (f ^ <*p*>)) = p by FINSEQ_1:42;

hence Suc (f ^ <*p*>) = p by Def2; :: thesis: Ant (f ^ <*p*>) = f

thus Ant (f ^ <*p*>) = f :: thesis: verum

proof

set fin = f ^ <*p*>;

then f = (f ^ <*p*>) | (dom f) by GRFUNC_1:23;

then f = (f ^ <*p*>) | (Seg (len f)) by FINSEQ_1:def 3;

hence Ant (f ^ <*p*>) = f by A1, Def1; :: thesis: verum

end;now :: thesis: for a being object st a in f holds

a in f ^ <*p*>

then
f c= f ^ <*p*>
;a in f ^ <*p*>

let a be object ; :: thesis: ( a in f implies a in f ^ <*p*> )

assume a in f ; :: thesis: a in f ^ <*p*>

then consider k being Nat such that

A2: k in dom f and

A3: a = [k,(f . k)] by FINSEQ_1:12;

( k in dom (f ^ <*p*>) & f . k = (f ^ <*p*>) . k ) by A2, FINSEQ_1:def 7, FINSEQ_2:15;

hence a in f ^ <*p*> by A3, FUNCT_1:1; :: thesis: verum

end;assume a in f ; :: thesis: a in f ^ <*p*>

then consider k being Nat such that

A2: k in dom f and

A3: a = [k,(f . k)] by FINSEQ_1:12;

( k in dom (f ^ <*p*>) & f . k = (f ^ <*p*>) . k ) by A2, FINSEQ_1:def 7, FINSEQ_2:15;

hence a in f ^ <*p*> by A3, FUNCT_1:1; :: thesis: verum

then f = (f ^ <*p*>) | (dom f) by GRFUNC_1:23;

then f = (f ^ <*p*>) | (Seg (len f)) by FINSEQ_1:def 3;

hence Ant (f ^ <*p*>) = f by A1, Def1; :: thesis: verum