let F be Field; :: thesis: for E being FieldExtension of F
for T1, T2, T3 being Subset of E st FAdj (F,T1) = FAdj (F,T2) holds
FAdj (F,(T1 \/ T3)) = FAdj (F,(T2 \/ T3))
let E be FieldExtension of F; :: thesis: for T1, T2, T3 being Subset of E st FAdj (F,T1) = FAdj (F,T2) holds
FAdj (F,(T1 \/ T3)) = FAdj (F,(T2 \/ T3))
let T1, T2, T3 be Subset of E; :: thesis: ( FAdj (F,T1) = FAdj (F,T2) implies FAdj (F,(T1 \/ T3)) = FAdj (F,(T2 \/ T3)) )
assume AS: FAdj (F,T1) = FAdj (F,T2) ; :: thesis: FAdj (F,(T1 \/ T3)) = FAdj (F,(T2 \/ T3))
reconsider Ea = E as FieldExtension of FAdj (F,T1) by FIELD_4:7;
reconsider T3a = T3 as Subset of Ea ;
reconsider Eb = E as FieldExtension of FAdj (F,T2) by FIELD_4:7;
reconsider T3b = T3 as Subset of Eb ;
thus FAdj (F,(T2 \/ T3)) = FAdj ((FAdj (F,T2)),T3b) by FIELD_13:18
.= FAdj (F,(T1 \/ T3)) by AS, FIELD_13:18 ; :: thesis: verum