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

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