let f, g be FinSequence; :: thesis: for x being set st x in dom g & f,g are_fiberwise_equipotent holds
ex y being set st
( y in dom g & f . x = g . y )
let x be set ; :: thesis: ( x in dom g & f,g are_fiberwise_equipotent implies ex y being set st
( y in dom g & f . x = g . y ) )
assume that
A1: x in dom g and
A2: f,g are_fiberwise_equipotent ; :: thesis: ex y being set st
( y in dom g & f . x = g . y )
consider P being Permutation of (dom g) such that
A3: f = g * P by A2, Th4;
take y = P . x; :: thesis: ( y in dom g & f . x = g . y )
thus y in dom g by A1, FUNCT_2:5; :: thesis: f . x = g . y
thus f . x = g . y by A1, A3, FUNCT_2:15; :: thesis: verum