let f, g be FinSequence; :: thesis: f ^ g,g ^ f are_fiberwise_equipotent
let y be set ; :: according to CLASSES1:def 9 :: thesis: card (Coim (f ^ g),y) = card (Coim (g ^ f),y)
thus card (Coim (f ^ g),y) = (card (g " {y})) + (card (f " {y})) by FINSEQ_3:63
.= card (Coim (g ^ f),y) by FINSEQ_3:63 ; :: thesis: verum