set X = { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
;
consider T being strict StableSubgroup of F2() such that
A2: P1[T] by A1;
A3: carr T in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
by A2;
then reconsider Y = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
as Subset of F2() by SETFAM_1:7;
A4: now :: thesis: for a being Element of F2() st a in Y holds
a " in Y
let a be Element of F2(); :: thesis: ( a in Y implies a " in Y )
assume A5: a in Y ; :: thesis: a " in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
holds
a " in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
implies a " in Z )

assume A6: Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
; :: thesis: a " in Z
then consider A being Subset of F2() such that
A7: A = Z and
A8: ex H being strict StableSubgroup of F2() st
( A = the carrier of H & P1[H] ) ;
consider H being StableSubgroup of F2() such that
A9: A = the carrier of H and
P1[H] by A8;
a in the carrier of H by ;
then a in H by STRUCT_0:def 5;
then a " in H by Lm19;
hence a " in Z by ; :: thesis: verum
end;
hence a " in Y by ; :: thesis: verum
end;
A10: now :: thesis: for a, b being Element of F2() st a in Y & b in Y holds
a * b in Y
let a, b be Element of F2(); :: thesis: ( a in Y & b in Y implies a * b in Y )
assume that
A11: a in Y and
A12: b in Y ; :: thesis: a * b in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
holds
a * b in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
implies a * b in Z )

assume A13: Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
; :: thesis: a * b in Z
then consider A being Subset of F2() such that
A14: A = Z and
A15: ex H being strict StableSubgroup of F2() st
( A = the carrier of H & P1[H] ) ;
consider H being StableSubgroup of F2() such that
A16: A = the carrier of H and
P1[H] by A15;
b in the carrier of H by ;
then A17: b in H by STRUCT_0:def 5;
a in the carrier of H by ;
then a in H by STRUCT_0:def 5;
then a * b in H by ;
hence a * b in Z by ; :: thesis: verum
end;
hence a * b in Y by ; :: thesis: verum
end;
A18: now :: thesis: for o being Element of F1()
for a being Element of F2() st a in Y holds
(F2() ^ o) . a in Y
let o be Element of F1(); :: thesis: for a being Element of F2() st a in Y holds
(F2() ^ o) . a in Y

let a be Element of F2(); :: thesis: ( a in Y implies (F2() ^ o) . a in Y )
assume A19: a in Y ; :: thesis: (F2() ^ o) . a in Y
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
holds
(F2() ^ o) . a in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
implies (F2() ^ o) . a in Z )

assume A20: Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
; :: thesis: (F2() ^ o) . a in Z
then consider A being Subset of F2() such that
A21: A = Z and
A22: ex H being strict StableSubgroup of F2() st
( A = the carrier of H & P1[H] ) ;
consider H being StableSubgroup of F2() such that
A23: A = the carrier of H and
P1[H] by A22;
a in the carrier of H by ;
then a in H by STRUCT_0:def 5;
then (F2() ^ o) . a in H by Lm9;
hence (F2() ^ o) . a in Z by ; :: thesis: verum
end;
hence (F2() ^ o) . a in Y by ; :: thesis: verum
end;
now :: thesis: for Z being set st Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
holds
1_ F2() in Z
let Z be set ; :: thesis: ( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
implies 1_ F2() in Z )

assume Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
; :: thesis: 1_ F2() in Z
then consider A being Subset of F2() such that
A24: Z = A and
A25: ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) ;
consider H being StableSubgroup of F2() such that
A26: A = the carrier of H and
P1[H] by A25;
1_ F2() in H by Lm17;
hence 1_ F2() in Z by ; :: thesis: verum
end;
then Y <> {} by ;
hence ex H being strict StableSubgroup of F2() st the carrier of H = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] )
}
by A10, A4, A18, Lm14; :: thesis: verum