let Ne, Ke be Subset of NAT ; :: thesis: for F being Function of Ne,Ke st rng F is finite holds
for I1, I2 being Function of Ne,Ke
for P1, P2 being Permutation of (rng F) st F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is "increasing & I2 is "increasing holds
( P1 = P2 & I1 = I2 )
let F be Function of Ne,Ke; :: thesis: ( rng F is finite implies for I1, I2 being Function of Ne,Ke
for P1, P2 being Permutation of (rng F) st F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is "increasing & I2 is "increasing holds
( P1 = P2 & I1 = I2 ) )
assume A1: rng F is finite ; :: thesis: for I1, I2 being Function of Ne,Ke
for P1, P2 being Permutation of (rng F) st F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is "increasing & I2 is "increasing holds
( P1 = P2 & I1 = I2 )
let I1, I2 be Function of Ne,Ke; :: thesis: for P1, P2 being Permutation of (rng F) st F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is "increasing & I2 is "increasing holds
( P1 = P2 & I1 = I2 )
let P1, P2 be Permutation of (rng F); :: thesis: ( F = P1 * I1 & F = P2 * I2 & rng F = rng I1 & rng F = rng I2 & I1 is "increasing & I2 is "increasing implies ( P1 = P2 & I1 = I2 ) )
assume that
A2: ( F = P1 * I1 & F = P2 * I2 ) and
A3: ( rng F = rng I1 & rng F = rng I2 ) and
A4: ( I1 is "increasing & I2 is "increasing ) ; :: thesis: ( P1 = P2 & I1 = I2 )
( rng F = {} implies rng F = {} ) ;
then ( dom P1 = rng F & dom P2 = rng F ) by FUNCT_2:def 1;
hence ( P1 = P2 & I1 = I2 ) by A1, A2, A3, A4, Th74; :: thesis: verum