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

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