let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds still_not-bound_in (f ^ g) = (still_not-bound_in f) \/ (still_not-bound_in g)
let f, g be FinSequence of CQC-WFF Al; :: thesis: still_not-bound_in (f ^ g) = (still_not-bound_in f) \/ (still_not-bound_in g)
thus still_not-bound_in (f ^ g) c= (still_not-bound_in f) \/ (still_not-bound_in g) :: according to XBOOLE_0:def 10 :: thesis: (still_not-bound_in f) \/ (still_not-bound_in g) c= still_not-bound_in (f ^ g)

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in still_not-bound_in (f ^ g) or b in (still_not-bound_in f) \/ (still_not-bound_in g) )
assume b in still_not-bound_in (f ^ g) ; :: thesis: b in (still_not-bound_in f) \/ (still_not-bound_in g)
then consider i being Nat, p being Element of CQC-WFF Al such that
A1: i in dom (f ^ g) and
A2: ( p = (f ^ g) . i & b in still_not-bound_in p ) by Def5;

A3: now :: thesis: ( ex n being Nat st
( n in dom g & i = (len f) + n ) implies b in (still_not-bound_in f) \/ (still_not-bound_in g) )

given n being Nat such that A4: n in dom g and
A5: i = (len f) + n ; :: thesis: b in (still_not-bound_in f) \/ (still_not-bound_in g)
(f ^ g) . i = g . n by A4, A5, FINSEQ_1:def 7;
then A6: b in still_not-bound_in g by A2, A4, Def5;
still_not-bound_in g c= (still_not-bound_in f) \/ (still_not-bound_in g) by XBOOLE_1:7;
hence b in (still_not-bound_in f) \/ (still_not-bound_in g) by A6; :: thesis: verum

end;

now :: thesis: ( i in dom f implies b in (still_not-bound_in f) \/ (still_not-bound_in g) )

assume A7: i in dom f ; :: thesis: b in (still_not-bound_in f) \/ (still_not-bound_in g)
then (f ^ g) . i = f . i by FINSEQ_1:def 7;
then A8: b in still_not-bound_in f by A2, A7, Def5;
still_not-bound_in f c= (still_not-bound_in f) \/ (still_not-bound_in g) by XBOOLE_1:7;
hence b in (still_not-bound_in f) \/ (still_not-bound_in g) by A8; :: thesis: verum

end;

hence b in (still_not-bound_in f) \/ (still_not-bound_in g) by A1, A3, FINSEQ_1:25; :: thesis: verum

end;

thus (still_not-bound_in f) \/ (still_not-bound_in g) c= still_not-bound_in (f ^ g) :: thesis: verum

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in (still_not-bound_in f) \/ (still_not-bound_in g) or b in still_not-bound_in (f ^ g) )
assume A9: b in (still_not-bound_in f) \/ (still_not-bound_in g) ; :: thesis: b in still_not-bound_in (f ^ g)

A10: now :: thesis: ( b in still_not-bound_in g implies b in still_not-bound_in (f ^ g) )

assume b in still_not-bound_in g ; :: thesis: b in still_not-bound_in (f ^ g)
then consider i being Nat, p being Element of CQC-WFF Al such that
A11: ( i in dom g & p = g . i ) and
A12: b in still_not-bound_in p by Def5;
( (len f) + i in dom (f ^ g) & p = (f ^ g) . ((len f) + i) ) by A11, FINSEQ_1:28, FINSEQ_1:def 7;
hence b in still_not-bound_in (f ^ g) by A12, Def5; :: thesis: verum

end;

now :: thesis: ( b in still_not-bound_in f implies b in still_not-bound_in (f ^ g) )

assume b in still_not-bound_in f ; :: thesis: b in still_not-bound_in (f ^ g)
then consider i being Nat, p being Element of CQC-WFF Al such that
A13: i in dom f and
A14: p = f . i and
A15: b in still_not-bound_in p by Def5;
( dom f c= dom (f ^ g) & p = (f ^ g) . i ) by A13, A14, FINSEQ_1:26, FINSEQ_1:def 7;
hence b in still_not-bound_in (f ^ g) by A13, A15, Def5; :: thesis: verum

end;

hence b in still_not-bound_in (f ^ g) by A9, A10, XBOOLE_0:def 3; :: thesis: verum

end;