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

let y be set ; :: thesis: card (Coim (h ^ f),y) = card (Coim (h ^ g),y)
card (Coim f,y) = card (Coim g,y) by A1, CLASSES1:def 9;
hence card (Coim (h ^ f),y) = (card (g " {y})) + (card (h " {y})) by FINSEQ_3:63
.= card (Coim (h ^ g),y) by FINSEQ_3:63 ;
:: thesis: verum

end;

hence h ^ f,h ^ g are_fiberwise_equipotent by CLASSES1:def 9; :: thesis: verum

end;

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

now

let x be set ; :: thesis: card (Coim f,x) = card (Coim g,x)
( card (Coim (h ^ f),x) = (card (Coim f,x)) + (card (h " {x})) & card ((h ^ g) " {x}) = (card (g " {x})) + (card (h " {x})) & card (Coim (h ^ f),x) = card (Coim (h ^ g),x) ) by A2, CLASSES1:def 9, FINSEQ_3:63;
hence card (Coim f,x) = card (Coim g,x) ; :: thesis: verum

end;

hence f,g are_fiberwise_equipotent by CLASSES1:def 9; :: thesis: verum