let n be Nat; :: thesis: for f1, f2 being natural-valued Function st n > 1 holds
( f1,f2 are_fiberwise_equipotent iff n |^ f1,n |^ f2 are_fiberwise_equipotent )
let f1, f2 be natural-valued Function; :: thesis: ( n > 1 implies ( f1,f2 are_fiberwise_equipotent iff n |^ f1,n |^ f2 are_fiberwise_equipotent ) )
assume A1: n > 1 ; :: thesis: ( f1,f2 are_fiberwise_equipotent iff n |^ f1,n |^ f2 are_fiberwise_equipotent )
set n1 = n |^ f1;
set n2 = n |^ f2;
thus ( f1,f2 are_fiberwise_equipotent implies n |^ f1,n |^ f2 are_fiberwise_equipotent ) :: thesis: ( n |^ f1,n |^ f2 are_fiberwise_equipotent implies f1,f2 are_fiberwise_equipotent )

proof

assume A2: f1,f2 are_fiberwise_equipotent ; :: thesis: n |^ f1,n |^ f2 are_fiberwise_equipotent
for x being object holds card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x))

proof

let x be object ; :: thesis: card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x))
A3: ( Coim ((n |^ f1),x) = (n |^ f1) " {x} & Coim ((n |^ f2),x) = (n |^ f2) " {x} ) by RELAT_1:def 17;
A4: ( dom (n |^ f1) = dom f1 & dom (n |^ f2) = dom f2 ) by Def4;

per cases ( ( not x in rng (n |^ f1) & not x in rng (n |^ f2) ) or ( x in rng (n |^ f1) & not x in rng (n |^ f2) ) or ( x in rng (n |^ f2) & not x in rng (n |^ f1) ) or ( x in rng (n |^ f1) & x in rng (n |^ f2) ) ) ;

suppose ( not x in rng (n |^ f1) & not x in rng (n |^ f2) ) ; :: thesis: card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x))

then ( (n |^ f1) " {x} = {} & (n |^ f2) " {x} = {} ) by FUNCT_1:72;
hence card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x)) by A3; :: thesis: verum

end;

suppose A5: ( x in rng (n |^ f1) & not x in rng (n |^ f2) ) ; :: thesis: card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x))

then consider y being object such that
A6: ( y in dom (n |^ f1) & (n |^ f1) . y = x ) by FUNCT_1:def 3;
A7: x = n to_power (f1 . y) by A6, A4, Def4;
f1 . y in rng f1 by A6, A4, FUNCT_1:def 3;
then f1 " {(f1 . y)} <> {} by FUNCT_1:72;
then A8: Coim (f1,(f1 . y)) <> {} by RELAT_1:def 17;
card (Coim (f1,(f1 . y))) = card (Coim (f2,(f1 . y))) by A2, CLASSES1:def 10;
then Coim (f2,(f1 . y)) <> {} by A8;
then f2 " {(f1 . y)} <> {} by RELAT_1:def 17;
then f1 . y in rng f2 by FUNCT_1:72;
then consider z being object such that
A9: ( z in dom f2 & f2 . z = f1 . y ) by FUNCT_1:def 3;
A10: z in dom (n |^ f2) by A9, Def4;
(n |^ f2) . z = x by A9, Def4, A7;
hence card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x)) by A10, FUNCT_1:def 3, A5; :: thesis: verum

end;

suppose A11: ( x in rng (n |^ f2) & not x in rng (n |^ f1) ) ; :: thesis: card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x))

then consider y being object such that
A12: ( y in dom (n |^ f2) & (n |^ f2) . y = x ) by FUNCT_1:def 3;
A13: x = n to_power (f2 . y) by A12, A4, Def4;
f2 . y in rng f2 by A12, A4, FUNCT_1:def 3;
then f2 " {(f2 . y)} <> {} by FUNCT_1:72;
then A14: Coim (f2,(f2 . y)) <> {} by RELAT_1:def 17;
card (Coim (f2,(f2 . y))) = card (Coim (f1,(f2 . y))) by A2, CLASSES1:def 10;
then Coim (f1,(f2 . y)) <> {} by A14;
then f1 " {(f2 . y)} <> {} by RELAT_1:def 17;
then f2 . y in rng f1 by FUNCT_1:72;
then consider z being object such that
A15: ( z in dom f1 & f1 . z = f2 . y ) by FUNCT_1:def 3;
A16: z in dom (n |^ f1) by A15, Def4;
(n |^ f1) . z = x by A15, Def4, A13;
hence card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x)) by A16, FUNCT_1:def 3, A11; :: thesis: verum

end;

suppose A17: ( x in rng (n |^ f1) & x in rng (n |^ f2) ) ; :: thesis: card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x))

then consider y1 being object such that
A18: ( y1 in dom (n |^ f1) & (n |^ f1) . y1 = x ) by FUNCT_1:def 3;
A19: x = n to_power (f1 . y1) by A18, A4, Def4;
consider y2 being object such that
A20: ( y2 in dom (n |^ f2) & (n |^ f2) . y2 = x ) by A17, FUNCT_1:def 3;
A21: x = n to_power (f2 . y2) by A20, A4, Def4;
then A22: f2 . y2 = f1 . y1 by A19, A1, PEPIN:30;
A23: Coim (f2,(f2 . y2)) = Coim ((n |^ f2),x) by A1, Th28, A21;
Coim (f1,(f1 . y1)) = Coim ((n |^ f1),x) by A1, Th28, A19;
hence card (Coim ((n |^ f1),x)) = card (Coim ((n |^ f2),x)) by A22, A2, CLASSES1:def 10, A23; :: thesis: verum

end;

end;

end;

hence n |^ f1,n |^ f2 are_fiberwise_equipotent by CLASSES1:def 10; :: thesis: verum

end;

assume A24: n |^ f1,n |^ f2 are_fiberwise_equipotent ; :: thesis: f1,f2 are_fiberwise_equipotent
for x being object holds card (Coim (f1,x)) = card (Coim (f2,x))

proof

let x be object ; :: thesis: card (Coim (f1,x)) = card (Coim (f2,x))
A25: ( Coim (f1,x) = f1 " {x} & Coim (f2,x) = f2 " {x} ) by RELAT_1:def 17;
A26: ( dom (n |^ f1) = dom f1 & dom (n |^ f2) = dom f2 ) by Def4;

per cases ( ( not x in rng f1 & not x in rng f2 ) or ( x in rng f1 & not x in rng f2 ) or ( x in rng f2 & not x in rng f1 ) or ( x in rng f1 & x in rng f2 ) ) ;

suppose ( not x in rng f1 & not x in rng f2 ) ; :: thesis: card (Coim (f1,x)) = card (Coim (f2,x))

then ( f1 " {x} = {} & f2 " {x} = {} ) by FUNCT_1:72;
hence card (Coim (f1,x)) = card (Coim (f2,x)) by A25; :: thesis: verum

end;

suppose A27: ( x in rng f1 & not x in rng f2 ) ; :: thesis: card (Coim (f1,x)) = card (Coim (f2,x))

then consider y being object such that
A28: ( y in dom f1 & f1 . y = x ) by FUNCT_1:def 3;
(n |^ f1) . y in rng (n |^ f1) by A26, A28, FUNCT_1:def 3;
then (n |^ f1) " {((n |^ f1) . y)} <> {} by FUNCT_1:72;
then A29: Coim ((n |^ f1),((n |^ f1) . y)) <> {} by RELAT_1:def 17;
card (Coim ((n |^ f1),((n |^ f1) . y))) = card (Coim ((n |^ f2),((n |^ f1) . y))) by A24, CLASSES1:def 10;
then Coim ((n |^ f2),((n |^ f1) . y)) <> {} by A29;
then (n |^ f2) " {((n |^ f1) . y)} <> {} by RELAT_1:def 17;
then (n |^ f1) . y in rng (n |^ f2) by FUNCT_1:72;
then consider z being object such that
A30: ( z in dom (n |^ f2) & (n |^ f2) . z = (n |^ f1) . y ) by FUNCT_1:def 3;
( (n |^ f2) . z = n to_power (f2 . z) & (n |^ f1) . y = n to_power (f1 . y) ) by A28, A30, A26, Def4;
then f2 . z = f1 . y by A30, A1, PEPIN:30;
hence card (Coim (f1,x)) = card (Coim (f2,x)) by A30, A26, A28, FUNCT_1:def 3, A27; :: thesis: verum

end;

suppose A31: ( x in rng f2 & not x in rng f1 ) ; :: thesis: card (Coim (f1,x)) = card (Coim (f2,x))

then consider y being object such that
A32: ( y in dom f2 & f2 . y = x ) by FUNCT_1:def 3;
(n |^ f2) . y in rng (n |^ f2) by A26, A32, FUNCT_1:def 3;
then (n |^ f2) " {((n |^ f2) . y)} <> {} by FUNCT_1:72;
then A33: Coim ((n |^ f2),((n |^ f2) . y)) <> {} by RELAT_1:def 17;
card (Coim ((n |^ f2),((n |^ f2) . y))) = card (Coim ((n |^ f1),((n |^ f2) . y))) by A24, CLASSES1:def 10;
then Coim ((n |^ f1),((n |^ f2) . y)) <> {} by A33;
then (n |^ f1) " {((n |^ f2) . y)} <> {} by RELAT_1:def 17;
then (n |^ f2) . y in rng (n |^ f1) by FUNCT_1:72;
then consider z being object such that
A34: ( z in dom (n |^ f1) & (n |^ f1) . z = (n |^ f2) . y ) by FUNCT_1:def 3;
( (n |^ f1) . z = n to_power (f1 . z) & (n |^ f2) . y = n to_power (f2 . y) ) by A32, A34, A26, Def4;
then f1 . z = f2 . y by A34, A1, PEPIN:30;
hence card (Coim (f1,x)) = card (Coim (f2,x)) by A34, A26, A32, FUNCT_1:def 3, A31; :: thesis: verum

end;

suppose A35: ( x in rng f1 & x in rng f2 ) ; :: thesis: card (Coim (f1,x)) = card (Coim (f2,x))

then consider y1 being object such that
A36: ( y1 in dom f1 & f1 . y1 = x ) by FUNCT_1:def 3;
A37: (n |^ f1) . y1 = n to_power (f1 . y1) by A36, Def4;
consider y2 being object such that
A38: ( y2 in dom f2 & f2 . y2 = x ) by A35, FUNCT_1:def 3;
A39: (n |^ f2) . y2 = n to_power (f2 . y2) by A38, Def4;
then A40: card (Coim ((n |^ f2),((n |^ f2) . y2))) = card (Coim ((n |^ f1),((n |^ f1) . y1))) by A37, A38, A36, A24, CLASSES1:def 10;
Coim (f2,(f2 . y2)) = Coim ((n |^ f2),((n |^ f2) . y2)) by A1, Th28, A39;
hence card (Coim (f1,x)) = card (Coim (f2,x)) by A1, Th28, A37, A40, A36, A38; :: thesis: verum

end;

end;

end;

hence f1,f2 are_fiberwise_equipotent by CLASSES1:def 10; :: thesis: verum