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

proof

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

now

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

end;

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

end;

assume A2: f ^ h,g ^ h 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 (f ^ h),x) = (card (Coim f,x)) + (card (Coim h,x)) & card (Coim (g ^ h),x) = (card (Coim g,x)) + (card (Coim h,x)) & card (Coim (f ^ h),x) = card (Coim (g ^ h),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