let F be Field; for E being FieldExtension of F
for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let E be FieldExtension of F; for b being Element of E
for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let b be Element of E; for T being Subset of E
for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let T be Subset of E; for E1 being FieldExtension of FAdj (F,T)
for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let E1 be FieldExtension of FAdj (F,T); for b1 being Element of E1 st E1 = E & b1 = b holds
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
let b1 be Element of E1; ( E1 = E & b1 = b implies FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1}) )
assume AS:
( E1 = E & b1 = b )
; FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
A1:
F is Subfield of FAdj ((FAdj (F,T)),{b1})
by FIELD_4:7;
{b} \/ T c= the carrier of (FAdj ((FAdj (F,T)),{b1}))
proof
now for o being object st o in {b} \/ T holds
o in the carrier of (FAdj ((FAdj (F,T)),{b1}))let o be
object ;
( o in {b} \/ T implies b1 in the carrier of (FAdj ((FAdj (F,T)),{b1})) )assume
o in {b} \/ T
;
b1 in the carrier of (FAdj ((FAdj (F,T)),{b1}))per cases then
( o in {b} or o in T )
by XBOOLE_0:def 3;
suppose B1:
o in T
;
b1 in the carrier of (FAdj ((FAdj (F,T)),{b1}))B2:
T is
Subset of
(FAdj (F,T))
by FIELD_6:35;
FAdj (
F,
T) is
Subfield of
FAdj (
(FAdj (F,T)),
{b1})
by FIELD_6:36;
then
the
carrier of
(FAdj (F,T)) c= the
carrier of
(FAdj ((FAdj (F,T)),{b1}))
by EC_PF_1:def 1;
hence
o in the
carrier of
(FAdj ((FAdj (F,T)),{b1}))
by B2, B1;
verum end; end; end;
hence
{b} \/ T c= the
carrier of
(FAdj ((FAdj (F,T)),{b1}))
;
verum
end;
then A:
FAdj (F,({b} \/ T)) is Subfield of FAdj ((FAdj (F,T)),{b1})
by AS, A1, FIELD_6:37;
A1:
FAdj (F,T) is Subfield of FAdj (F,({b} \/ T))
by ext0, XBOOLE_1:7;
{b} \/ T is Subset of (FAdj (F,({b} \/ T)))
by FIELD_6:35;
then
{b1} c= the carrier of (FAdj (F,({b} \/ T)))
by AS, XBOOLE_1:11;
then
FAdj ((FAdj (F,T)),{b1}) is Subfield of FAdj (F,({b} \/ T))
by A1, AS, FIELD_6:37;
hence
FAdj (F,({b} \/ T)) = FAdj ((FAdj (F,T)),{b1})
by A, EC_PF_1:4; verum