let X, N, I be non empty set ; 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; 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; ( 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
; 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; (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; verum