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:18;
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:19
.= bound_QC-variables \/ {x} by FUNCT_2:67
.= bound_QC-variables by ZFMISC_1:46 ;
hence h +* (x .--> (x. k)) is Function of bound_QC-variables ,bound_QC-variables by A1, A3, FUNCT_2:4, XBOOLE_1:1; :: thesis: verum