let G be Group; :: thesis: for N being finite Subset of (the_normal_subgroups_of G)
for n being Nat st n = card N holds
canFS N is normal Subgroup-Family of Seg n,G
let N be finite Subset of (the_normal_subgroups_of G); :: thesis: for n being Nat st n = card N holds
canFS N is normal Subgroup-Family of Seg n,G
let n be Nat; :: thesis: ( n = card N implies canFS N is normal Subgroup-Family of Seg n,G )
assume A1: n = card N ; :: thesis: canFS N is normal Subgroup-Family of Seg n,G
len (canFS N) = n by A1, FINSEQ_1:93;
then A2: dom (canFS N) = Seg n by FINSEQ_1:def 3;
the_normal_subgroups_of G c= Subgroups G by GRNILP_1:17;
then A3: N is finite Subset of (Subgroups G) by XBOOLE_1:1;
for i being object st i in Seg n holds
(canFS N) . i is normal Subgroup of G

proof

let i be object ; :: thesis: ( i in Seg n implies (canFS N) . i is normal Subgroup of G )
assume i in Seg n ; :: thesis: (canFS N) . i is normal Subgroup of G
then (canFS N) . i in rng (canFS N) by A2, FUNCT_1:3;
then (canFS N) . i in N by FINSEQ_1:def 4, TARSKI:def 3;
hence (canFS N) . i is normal Subgroup of G by GRNILP_1:def 1; :: thesis: verum

end;

hence canFS N is normal Subgroup-Family of Seg n,G by A1, A3, Def18, ThCanSubgrFam; :: thesis: verum