let Ke, Ne 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 and
A3: F = P2 * I2 and
A4: rng F = rng I1 and
A5: rng F = rng I2 and
A6: I1 is 'increasing and
A7: I2 is 'increasing ; :: thesis: ( P1 = P2 & I1 = I2 )
A8: ( rng F = {} implies rng F = {} ) ;
then A9: dom P2 = rng F by FUNCT_2:def 1;
dom P1 = rng F by A8, FUNCT_2:def 1;
hence ( P1 = P2 & I1 = I2 ) by A1, A2, A3, A4, A5, A6, A7, A9, Th64; :: thesis: verum