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