let p be QC-formula; :: thesis: for d being Subset of bound_QC-variables holds
( d = H₁(p) iff ex F being Function of QC-WFF ,(bool bound_QC-variables ) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = H₂(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₃(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₄(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₅(p,d1) ) ) ) ) )
let d be Subset of bound_QC-variables ; :: thesis: ( d = H₁(p) iff ex F being Function of QC-WFF ,(bool bound_QC-variables ) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = H₂(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₃(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₄(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₅(p,d1) ) ) ) ) )
thus ( d = still_not-bound_in p implies ex F being Function of QC-WFF ,(bool bound_QC-variables ) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) ) :: thesis: ( ex F being Function of QC-WFF ,(bool bound_QC-variables ) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = H₂(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₃(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₄(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₅(p,d1) ) ) ) ) implies d = H₁(p) )

proof

assume d = still_not-bound_in p ; :: thesis: ex F being Function of QC-WFF ,(bool bound_QC-variables ) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )
then consider F being Function of QC-WFF ,(bool bound_QC-variables ) such that
A1: ( d = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) by QC_LANG1:def 29;
take F ; :: thesis: ( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )
thus d = F . p by A1; :: thesis: for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
let p be Element of QC-WFF ; :: thesis: for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
let d1, d2 be Subset of bound_QC-variables ; :: thesis: ( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
thus ( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) ) by A1; :: thesis: ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
thus ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) by A1; :: thesis: verum

end;

given F being Function of QC-WFF ,(bool bound_QC-variables ) such that A2: d = F . p and
A3: for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ; :: thesis: d = H₁(p)

now

let p be Element of QC-WFF ; :: thesis: ( F . VERUM = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus F . VERUM = {} by A3; :: thesis: ( ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ) :: thesis: ( ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )

proof

assume p is atomic ; :: thesis: F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) }
then F . p = still_not-bound_in (the_arguments_of p) by A3;
hence F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables ) } ; :: thesis: verum

end;

thus ( p is negative implies F . p = F . (the_argument_of p) ) by A3; :: thesis: ( ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A3; :: thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} )
assume p is universal ; :: thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)}
hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A3; :: thesis: verum

end;

hence d = H₁(p) by A2, QC_LANG1:def 29; :: thesis: verum