let x be Element of bound_QC-variables ; :: thesis: for k being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds h +* (x .--> (x. k)) is Function of bound_QC-variables,bound_QC-variables
let k be Element of NAT ; :: thesis: for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds h +* (x .--> (x. k)) is Function of bound_QC-variables,bound_QC-variables
let h be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis: h +* (x .--> (x. k)) is Function of bound_QC-variables,bound_QC-variables
A1: rng (h +* (x .--> (x. k))) c= (rng h) \/ (rng (x .--> (x. k))) by FUNCT_4:17;
A2: rng (x .--> (x. k)) c= bound_QC-variables by RELAT_1:def 19;
rng h c= bound_QC-variables by RELAT_1:def 19;
then A3: (rng h) \/ (rng (x .--> (x. k))) c= bound_QC-variables by A2, XBOOLE_1:8;
dom (h +* (x .--> (x. k))) = (dom h) \/ (dom ({x} --> (x. k))) by FUNCT_4:def 1
.= (dom h) \/ {x} by FUNCOP_1:13
.= bound_QC-variables \/ {x} by FUNCT_2:52
.= bound_QC-variables by ZFMISC_1:40 ;
hence h +* (x .--> (x. k)) is Function of bound_QC-variables,bound_QC-variables by A1, A3, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum