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

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