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 A1: b in still_not-bound_in (f ^ g) ; :: thesis: b in (still_not-bound_in f) \/ (still_not-bound_in g)
consider i being Element of NAT , p being Element of CQC-WFF such that
A2: ( i in dom (f ^ g) & p = (f ^ g) . i & b in still_not-bound_in p ) by A1, Def5;

A3: now

assume A4: 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 A5: b in still_not-bound_in f by A2, A4, 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 A5; :: thesis: verum

end;

now

given n being Nat such that A6: ( n in dom g & i = (len f) + n ) ; :: thesis: b in (still_not-bound_in f) \/ (still_not-bound_in g)
(f ^ g) . i = g . n by A6, FINSEQ_1:def 7;
then A7: b in still_not-bound_in g by A2, A6, 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 A7; :: thesis: verum

end;

hence b in (still_not-bound_in f) \/ (still_not-bound_in g) by A2, 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 A8: b in (still_not-bound_in f) \/ (still_not-bound_in g) ; :: thesis: b in still_not-bound_in (f ^ g)

A9: 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
A10: ( i in dom f & p = f . i & b in still_not-bound_in p ) by Def5;
A11: dom f c= dom (f ^ g) by FINSEQ_1:39;
p = (f ^ g) . i by A10, FINSEQ_1:def 7;
hence b in still_not-bound_in (f ^ g) by A10, A11, Def5; :: thesis: verum

end;

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
A12: ( i in dom g & p = g . i & b in still_not-bound_in p ) by Def5;
A13: (len f) + i in dom (f ^ g) by A12, FINSEQ_1:41;
p = (f ^ g) . ((len f) + i) by A12, FINSEQ_1:def 7;
hence b in still_not-bound_in (f ^ g) by A12, A13, Def5; :: thesis: verum

end;

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

end;