let f, g be FinSequence of INT ; :: thesis: for m, n being Nat st 1 <= n & n <= len f & 1 <= m & m <= len f & g = (f +* (m,(f /. n))) +* (n,(f /. m)) holds
( f . m = g . n & f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent )
let m, n be Nat; :: thesis: ( 1 <= n & n <= len f & 1 <= m & m <= len f & g = (f +* (m,(f /. n))) +* (n,(f /. m)) implies ( f . m = g . n & f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent ) )
assume that
A1: ( 1 <= n & n <= len f ) and
A2: ( 1 <= m & m <= len f ) and
A3: g = (f +* (m,(f /. n))) +* (n,(f /. m)) ; :: thesis: ( f . m = g . n & f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent )
A4: dom (f +* (m,(f /. n))) = dom f by Th29;
A5: n in dom f by A1, FINSEQ_3:25;
hence A6: g . n = f /. m by A3, A4, Th30
.= f . m by A2, FINSEQ_4:15 ;
:: thesis: ( f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent )
A7: m in dom f by A2, FINSEQ_3:25;

hereby :: thesis: ( ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent )

per cases ( m = n or m <> n ) ;

suppose m = n ; :: thesis: g . m = f . n

hence g . m = f . n by A6; :: thesis: verum

end;

suppose m <> n ; :: thesis: g . m = f . n

hence g . m = (f +* (m,(f /. n))) . m by A3, Th31
.= f /. n by A7, Th30
.= f . n by A1, FINSEQ_4:15 ;
:: thesis: verum

end;

end;

end;

A9: now :: thesis: for k being set st k <> m & k <> n & k in dom f holds
g . k = f . k

let k be set ; :: thesis: ( k <> m & k <> n & k in dom f implies g . k = f . k )
assume that
A10: k <> m and
A11: k <> n and
k in dom f ; :: thesis: g . k = f . k
thus g . k = (f +* (m,(f /. n))) . k by A3, A11, Th31
.= f . k by A10, Th31 ; :: thesis: verum

end;

dom g = dom f by A3, A4, Th29;
hence ( ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent ) by A5, A7, A6, A8, A9, RFINSEQ:28; :: thesis: verum