let G be Group; :: thesis: for S being finite Subset of (Subgroups G)
for n being Nat st n = card S holds
canFS S is Subgroup-Family of Seg n,G
let S be finite Subset of (Subgroups G); :: thesis: for n being Nat st n = card S holds
canFS S is Subgroup-Family of Seg n,G
let n be Nat; :: thesis: ( n = card S implies canFS S is Subgroup-Family of Seg n,G )
assume A1: n = card S ; :: thesis: canFS S is Subgroup-Family of Seg n,G
len (canFS S) = n by A1, FINSEQ_1:93;
then A2: dom (canFS S) = Seg n by FINSEQ_1:def 3;
for y being object st y in rng (canFS S) holds
y is Subgroup of G

proof

let y be object ; :: thesis: ( y in rng (canFS S) implies y is Subgroup of G )
assume y in rng (canFS S) ; :: thesis: y is Subgroup of G
then y in S by FINSEQ_1:def 4, TARSKI:def 3;
hence y is Subgroup of G by GROUP_3:def 1; :: thesis: verum

end;

then canFS S is Group-yielding ;
then A5: canFS S is Group-Family of Seg n by A1, ThCanFSIsMss;
for i being object st i in Seg n holds
(canFS S) . i is Subgroup of G

proof

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

end;

hence canFS S is Subgroup-Family of Seg n,G by A5, GROUP_20:def 1; :: thesis: verum