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)

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

thus
(still_not-bound_in f) \/ (still_not-bound_in g) c= still_not-bound_in (f ^ g)
:: thesis: verum
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;

end;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) )

( 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;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

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

hence
b in (still_not-bound_in f) \/ (still_not-bound_in g)
by A1, A3, FINSEQ_1:25; :: thesis: verumassume 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;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

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)

end;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;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

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

hence
b in still_not-bound_in (f ^ g)
by A9, A10, XBOOLE_0:def 3; :: thesis: verumassume
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;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