let f, g, h be FinSequence; ( 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 )
( f ^ h,g ^ h are_fiberwise_equipotent implies f,g are_fiberwise_equipotent )
assume A2:
f ^ h,g ^ h are_fiberwise_equipotent
; f,g are_fiberwise_equipotent
now for x being object holds card (Coim (f,x)) = card (Coim (g,x))let x be
object ;
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;
verum end;
hence
f,g are_fiberwise_equipotent
; verum