let X, N, I be non empty set ; :: thesis: for s being Function of X,I
for c being Function of X,N st c is one-to-one holds
for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I
let s be Function of X,I; :: thesis: for c being Function of X,N st c is one-to-one holds
for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I
let c be Function of X,N; :: thesis: ( c is one-to-one implies for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I )
assume c is one-to-one ; :: thesis: for n being Element of I holds (N --> n) +* (s * (c ")) is Function of N,I
then A1: dom (c ") = rng c by FUNCT_1:33;
let n be Element of I; :: thesis: (N --> n) +* (s * (c ")) is Function of N,I
set f = N --> n;
set g = s * (c ");
A2: dom (s * (c ")) c= dom (c ") by RELAT_1:25;
rng (s * (c ")) c= rng s by RELAT_1:26;
then rng (s * (c ")) c= I by XBOOLE_1:1;
then A3: (rng (N --> n)) \/ (rng (s * (c "))) c= I by XBOOLE_1:8;
A5: rng ((N --> n) +* (s * (c "))) c= (rng (N --> n)) \/ (rng (s * (c "))) by FUNCT_4:17;
dom ((N --> n) +* (s * (c "))) = (dom (N --> n)) \/ (dom (s * (c "))) by FUNCT_4:def 1;
then dom ((N --> n) +* (s * (c "))) = N by A2, A1, XBOOLE_1:1, XBOOLE_1:12;
hence (N --> n) +* (s * (c ")) is Function of N,I by A5, A3, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum