let f, g be FinSequence of INT ; :: thesis: for m, n being Nat st 1 <= n & n <= len f & 1 <= m & m <= len f & len f = len g & f . m = g . n & f . n = g . m & ( for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds

f . k = g . k ) holds

f,g are_fiberwise_equipotent

let m, n be Nat; :: thesis: ( 1 <= n & n <= len f & 1 <= m & m <= len f & len f = len g & f . m = g . n & f . n = g . m & ( for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds

f . k = g . k ) implies f,g are_fiberwise_equipotent )

assume that

A1: ( 1 <= n & n <= len f ) and

A2: ( 1 <= m & m <= len f ) and

A3: len f = len g and

A4: ( f . m = g . n & f . n = g . m ) and

A5: for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds

f . k = g . k ; :: thesis: f,g are_fiberwise_equipotent

A6: m in Seg (len f) by A2, FINSEQ_1:1;

A7: Seg (len f) = dom f by FINSEQ_1:def 3;

hence f,g are_fiberwise_equipotent by A4, A7, A6, A8, RFINSEQ:28; :: thesis: verum

f . k = g . k ) holds

f,g are_fiberwise_equipotent

let m, n be Nat; :: thesis: ( 1 <= n & n <= len f & 1 <= m & m <= len f & len f = len g & f . m = g . n & f . n = g . m & ( for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds

f . k = g . k ) implies f,g are_fiberwise_equipotent )

assume that

A1: ( 1 <= n & n <= len f ) and

A2: ( 1 <= m & m <= len f ) and

A3: len f = len g and

A4: ( f . m = g . n & f . n = g . m ) and

A5: for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds

f . k = g . k ; :: thesis: f,g are_fiberwise_equipotent

A6: m in Seg (len f) by A2, FINSEQ_1:1;

A7: Seg (len f) = dom f by FINSEQ_1:def 3;

A8: now :: thesis: for k being set st k <> m & k <> n & k in dom f holds

f . k = g . k

( n in dom f & dom f = dom g )
by A1, A3, A7, FINSEQ_1:1, FINSEQ_1:def 3;f . k = g . k

let k be set ; :: thesis: ( k <> m & k <> n & k in dom f implies f . k = g . k )

assume that

A9: ( k <> m & k <> n ) and

A10: k in dom f ; :: thesis: f . k = g . k

reconsider i = k as Nat by A10;

( 1 <= i & i <= len f ) by A7, A10, FINSEQ_1:1;

hence f . k = g . k by A5, A9; :: thesis: verum

end;assume that

A9: ( k <> m & k <> n ) and

A10: k in dom f ; :: thesis: f . k = g . k

reconsider i = k as Nat by A10;

( 1 <= i & i <= len f ) by A7, A10, FINSEQ_1:1;

hence f . k = g . k by A5, A9; :: thesis: verum

hence f,g are_fiberwise_equipotent by A4, A7, A6, A8, RFINSEQ:28; :: thesis: verum