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 Z0: c is one-to-one ; :: thesis: for n being Element of I holds (N --> n) +* (s * (c " )) is Function of N,I
let n be Element of I; :: thesis: (N --> n) +* (s * (c " )) is Function of N,I
set f = N --> n;
set g = s * (c " );
Z1: dom ((N --> n) +* (s * (c " ))) = (dom (N --> n)) \/ (dom (s * (c " ))) by FUNCT_4:def 1;
Z2: ( dom (s * (c " )) c= dom (c " ) & rng (s * (c " )) c= rng s ) by RELAT_1:44, RELAT_1:45;
Z3: ( dom (N --> n) = N & rng (N --> n) = {n} ) by FUNCOP_1:14, FUNCOP_1:19;
( dom (c " ) = rng c & rng c c= N ) by Z0, FUNCT_1:55;
then Z4: dom ((N --> n) +* (s * (c " ))) = N by Z1, Z2, Z3, XBOOLE_1:1, XBOOLE_1:12;
rng (s * (c " )) c= I by Z2, XBOOLE_1:1;
then ( rng ((N --> n) +* (s * (c " ))) c= (rng (N --> n)) \/ (rng (s * (c " ))) & (rng (N --> n)) \/ (rng (s * (c " ))) c= I ) by FUNCT_4:18, XBOOLE_1:8;
hence (N --> n) +* (s * (c " )) is Function of N,I by Z4, FUNCT_2:4, XBOOLE_1:1; :: thesis: verum