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 A1: ( x in dom g & f,g are_fiberwise_equipotent ) ; :: thesis: ex y being set st
( y in dom g & f . x = g . y )
then consider P being Permutation of (dom g) such that
A2: f = g * P by Th17;
take y = P . x; :: thesis: ( y in dom g & f . x = g . y )
thus y in dom g by A1, FUNCT_2:7; :: thesis: f . x = g . y
thus f . x = g . y by A1, A2, FUNCT_2:21; :: thesis: verum