let F be Field; :: thesis: for E being FieldExtension of F
for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
let E be FieldExtension of F; :: thesis: for L being F -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
let L be F -monomorphic Field; :: thesis: for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
let f be Monomorphism of F,L; :: thesis: for S being non empty ascending Subset of (Ext_Set (f,E))
for p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
let S be non empty ascending Subset of (Ext_Set (f,E)); :: thesis: for p being Element of S holds
( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
let p be Element of S; :: thesis: ( 1. (unionField (S,f,E)) = 1. (p `1) & 0. (unionField (S,f,E)) = 0. (p `1) )
1. (unionField (S,f,E)) = unionOne (S,f,E) by duf;
then consider q being Element of S such that
A: 1. (unionField (S,f,E)) = 1. (q `1) by defone;

now :: thesis: 1. (unionField (S,f,E)) = 1. (p `1)

per cases ( p <= q or q <= p ) by dasc;

suppose p <= q ; :: thesis: 1. (unionField (S,f,E)) = 1. (p `1)

then p `1 is Subfield of q `1 by FIELD_4:7;
hence 1. (unionField (S,f,E)) = 1. (p `1) by A, EC_PF_1:def 1; :: thesis: verum

end;

suppose q <= p ; :: thesis: 1. (unionField (S,f,E)) = 1. (p `1)

then q `1 is Subfield of p `1 by FIELD_4:7;
hence 1. (unionField (S,f,E)) = 1. (p `1) by A, EC_PF_1:def 1; :: thesis: verum

end;

end;

end;

hence 1. (unionField (S,f,E)) = 1. (p `1) ; :: thesis: 0. (unionField (S,f,E)) = 0. (p `1)
0. (unionField (S,f,E)) = unionZero (S,f,E) by duf;
then consider q being Element of S such that
A: 0. (unionField (S,f,E)) = 0. (q `1) by defzero;

now :: thesis: 0. (unionField (S,f,E)) = 0. (p `1)

per cases ( p <= q or q <= p ) by dasc;

suppose p <= q ; :: thesis: 0. (unionField (S,f,E)) = 0. (p `1)

then p `1 is Subfield of q `1 by FIELD_4:7;
hence 0. (unionField (S,f,E)) = 0. (p `1) by A, EC_PF_1:def 1; :: thesis: verum

end;

suppose q <= p ; :: thesis: 0. (unionField (S,f,E)) = 0. (p `1)

then q `1 is Subfield of p `1 by FIELD_4:7;
hence 0. (unionField (S,f,E)) = 0. (p `1) by A, EC_PF_1:def 1; :: thesis: verum

end;

end;

end;

hence 0. (unionField (S,f,E)) = 0. (p `1) ; :: thesis: verum