let f, g be FinSequence; :: thesis: ( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P )

thus ( f,g are_fiberwise_equipotent implies ex P being Permutation of (dom g) st f = g * P ) :: thesis: ( ex P being Permutation of (dom g) st f = g * P implies f,g are_fiberwise_equipotent )

( dom g = {} implies dom g = {} ) ;

then ( rng P c= dom g & dom P = dom g ) by FUNCT_2:def 1;

then dom f = dom g by A2, RELAT_1:27;

hence f,g are_fiberwise_equipotent by A2, CLASSES1:80; :: thesis: verum

thus ( f,g are_fiberwise_equipotent implies ex P being Permutation of (dom g) st f = g * P ) :: thesis: ( ex P being Permutation of (dom g) st f = g * P implies f,g are_fiberwise_equipotent )

proof

given P being Permutation of (dom g) such that A2:
f = g * P
; :: thesis: f,g are_fiberwise_equipotent
assume A1:
f,g are_fiberwise_equipotent
; :: thesis: ex P being Permutation of (dom g) st f = g * P

then dom f = dom g by Th3;

hence ex P being Permutation of (dom g) st f = g * P by A1, CLASSES1:80; :: thesis: verum

end;then dom f = dom g by Th3;

hence ex P being Permutation of (dom g) st f = g * P by A1, CLASSES1:80; :: thesis: verum

( dom g = {} implies dom g = {} ) ;

then ( rng P c= dom g & dom P = dom g ) by FUNCT_2:def 1;

then dom f = dom g by A2, RELAT_1:27;

hence f,g are_fiberwise_equipotent by A2, CLASSES1:80; :: thesis: verum