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 :: thesis: for y being object holds card (Coim ((f ^ h),y)) = card (Coim ((g ^ h),y))

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

end;

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

end;

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