let f, g be FinSequence; :: thesis: f ^ g,g ^ f are_fiberwise_equipotent
let y be object ; :: according to CLASSES1:def 10 :: 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:57
.= card (Coim ((g ^ f),y)) by FINSEQ_3:57 ; :: thesis: verum