let f, g be FinSequence of CQC-WFF ; :: 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 set ; :: 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 Element of NAT , p being Element of CQC-WFF 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

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

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:38; :: 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 set ; :: 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

assume b in still_not-bound_in g ; :: thesis: b in still_not-bound_in (f ^ g)
then consider i being Element of NAT , p being Element of CQC-WFF 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:41, FINSEQ_1:def 7;
hence b in still_not-bound_in (f ^ g) by A12, Def5; :: thesis: verum

end;

now

assume b in still_not-bound_in f ; :: thesis: b in still_not-bound_in (f ^ g)
then consider i being Element of NAT , p being Element of CQC-WFF 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:39, 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;