let f, g, h be FinSequence; :: thesis: ( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )
thus ( f,g are_fiberwise_equipotent implies h ^ f,h ^ g are_fiberwise_equipotent ) :: thesis: ( h ^ f,h ^ g are_fiberwise_equipotent implies f,g are_fiberwise_equipotent )

proof

assume A1: f,g are_fiberwise_equipotent ; :: thesis: h ^ f,h ^ g are_fiberwise_equipotent

now :: thesis: for y being object holds card (Coim ((h ^ f),y)) = card (Coim ((h ^ g),y))

let y be object ; :: thesis: card (Coim ((h ^ f),y)) = card (Coim ((h ^ g),y))
card (Coim (f,y)) = card (Coim (g,y)) by A1;
hence card (Coim ((h ^ f),y)) = (card (g " {y})) + (card (h " {y})) by FINSEQ_3:57
.= card (Coim ((h ^ g),y)) by FINSEQ_3:57 ;
:: thesis: verum

end;

hence h ^ f,h ^ g are_fiberwise_equipotent ; :: thesis: verum

end;

assume A2: h ^ f,h ^ g are_fiberwise_equipotent ; :: thesis: f,g are_fiberwise_equipotent

now :: thesis: for x being object holds card (Coim (f,x)) = card (Coim (g,x))

let x be object ; :: thesis: card (Coim (f,x)) = card (Coim (g,x))
A3: ( card (Coim ((h ^ f),x)) = (card (Coim (f,x))) + (card (h " {x})) & card ((h ^ g) " {x}) = (card (g " {x})) + (card (h " {x})) ) by FINSEQ_3:57;
card (Coim ((h ^ f),x)) = card (Coim ((h ^ g),x)) by A2;
hence card (Coim (f,x)) = card (Coim (g,x)) by A3; :: thesis: verum

end;

hence f,g are_fiberwise_equipotent ; :: thesis: verum