let u, v be QC-symbol of A; :: thesis: ( ex f being sequence of (QC-symbols A) st
( u = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) & ex f being sequence of (QC-symbols A) st
( v = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) implies u = v )
assume A2: ( ex f being sequence of (QC-symbols A) st
( f . n = u & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) & ex g being sequence of (QC-symbols A) st
( g . n = v & g . 0 = t & ( for k being Nat holds g . (k + 1) = (g . k) ++ ) ) ) ; :: thesis: u = v
consider f being sequence of (QC-symbols A) such that
A3: ( f . n = u & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) by A2;
consider g being sequence of (QC-symbols A) such that
A4: ( g . n = v & g . 0 = t & ( for k being Nat holds g . (k + 1) = (g . k) ++ ) ) by A2;
defpred S₁[ Nat] means f . $1 = g . $1;
A5: S₁[ 0 ] by A3, A4;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
thus f . (k + 1) = (f . k) ++ by A3
.= g . (k + 1) by A4, A7 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence u = v by A3, A4; :: thesis: verum