let F1, F2 be finite Field; :: thesis: ( order F1 = order F2 implies F1,F2 are_isomorphic )
assume AS: order F1 = order F2 ; :: thesis: F1,F2 are_isomorphic
consider p1 being Prime, n1 being non zero Nat such that
A: ( Char F1 = p1 & order F1 = p1 |^ n1 ) by finex2;
consider p2 being Prime, n2 being non zero Nat such that
B: ( Char F2 = p2 & order F2 = p2 |^ n2 ) by finex2;
set PF1 = PrimeField F1;
set PF2 = PrimeField F2;
( p1 = p2 & n1 = n2 ) by AS, A, B, lemp;
then ( PrimeField F1, Z/ p1 are_isomorphic & Z/ p1, PrimeField F2 are_isomorphic ) by A, B, RING_3:114;
then PrimeField F1, PrimeField F2 are_isomorphic by RING_3:44;
then consider i being Function of (PrimeField F1),(PrimeField F2) such that
I: i is RingIsomorphism ;
reconsider PF2 = PrimeField F2 as PrimeField F1 -homomorphic PrimeField F1 -isomorphic Field by I, RING_2:def 4, RING_3:def 4;
reconsider i = i as Isomorphism of (PrimeField F1),PF2 by I;
reconsider E1 = F1 as SplittingField of X^ ((p1 |^ n1),(PrimeField F1)) by A, split;
set E2 = the SplittingField of (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1)));
consider f being Function of E1, the SplittingField of (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))) such that
D: ( f is i -extending & f is isomorphism ) by FIELD_8:57;
E: E1, the SplittingField of (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))) are_isomorphic by D;
F: (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))) = X^ ((p2 |^ n2),PF2)

proof

reconsider q = (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))) as Polynomial of PF2 ;
set r1 = X^ ((p1 |^ n1),(PrimeField F1));
set r2 = X^ ((p2 |^ n2),PF2);

now :: thesis: for k being Nat holds q . k = (X^ ((p2 |^ n2),PF2)) . k

let k be Nat; :: thesis: q . b₁ = (X^ ((p2 |^ n2),PF2)) . b₁

per cases ( k = 1 or k = p1 |^ n1 or ( k <> 1 & k <> p1 |^ n1 ) ) ;

suppose H: k = 1 ; :: thesis: q . b₁ = (X^ ((p2 |^ n2),PF2)) . b₁

hence q . k = i . ((X^ ((p1 |^ n1),(PrimeField F1))) . 1) by FIELD_1:def 2
.= i . (- (1. (PrimeField F1))) by Lm10
.= - (i . (1_ (PrimeField F1))) by RING_2:7
.= - (1_ PF2) by GROUP_1:def 13
.= (X^ ((p2 |^ n2),PF2)) . k by H, Lm10 ;
:: thesis: verum

end;

suppose H: k = p1 |^ n1 ; :: thesis: q . b₁ = (X^ ((p2 |^ n2),PF2)) . b₁

thus q . k = i . ((X^ ((p1 |^ n1),(PrimeField F1))) . k) by FIELD_1:def 2
.= i . (1_ (PrimeField F1)) by H, Lm10
.= 1_ PF2 by GROUP_1:def 13
.= (X^ ((p2 |^ n2),PF2)) . k by H, AS, A, B, Lm10 ; :: thesis: verum

end;

suppose H: ( k <> 1 & k <> p1 |^ n1 ) ; :: thesis: q . b₁ = (X^ ((p2 |^ n2),PF2)) . b₁

thus q . k = i . ((X^ ((p1 |^ n1),(PrimeField F1))) . k) by FIELD_1:def 2
.= i . (0. (PrimeField F1)) by H, Lm11
.= 0. PF2 by RING_2:6
.= (X^ ((p2 |^ n2),PF2)) . k by H, AS, A, B, Lm11 ; :: thesis: verum

end;

end;

end;

hence (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))) = X^ ((p2 |^ n2),PF2) ; :: thesis: verum

end;

reconsider E3 = F2 as SplittingField of X^ ((p2 |^ n2),PF2) by B, split;
the SplittingField of (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))),E3 are_isomorphic_over PF2 by F, FIELD_8:58;
then consider g being Function of the SplittingField of (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))),E3 such that
G: g is isomorphism by FIELD_8:def 5;
the SplittingField of (PolyHom i) . (X^ ((p1 |^ n1),(PrimeField F1))),E3 are_isomorphic by G;
hence F1,F2 are_isomorphic by E, RING_3:44; :: thesis: verum