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;
A8: now :: thesis: for k being set st k <> m & k <> n & k in dom f holds
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;
( n in dom f & dom f = dom g ) by A1, A3, A7, FINSEQ_1:1, FINSEQ_1:def 3;
hence f,g are_fiberwise_equipotent by A4, A7, A6, A8, RFINSEQ:28; :: thesis: verum