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:55;
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:44;
rng (s * (c " )) c= rng s by RELAT_1:45;
then rng (s * (c " )) c= I by XBOOLE_1:1;
then A3: (rng (N --> n)) \/ (rng (s * (c " ))) c= I by XBOOLE_1:8;
A4: dom (N --> n) = N by FUNCOP_1:19;
A5: rng ((N --> n) +* (s * (c " ))) c= (rng (N --> n)) \/ (rng (s * (c " ))) by FUNCT_4:18;
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, A4, A1, XBOOLE_1:1, XBOOLE_1:12;
hence (N --> n) +* (s * (c " )) is Function of N,I by A5, A3, FUNCT_2:4, XBOOLE_1:1; :: thesis: verum