let G be Group; :: thesis:
let F be FinSequence of the carrier of G; :: thesis:
defpred S₁[ FinSequence of the carrier of G] means Product ($1 - {(1_ G)}) = Product $1;
A1: for F being FinSequence of the carrier of G
for a being Element of G st S₁[F] holds
S₁[F ^ <*a*>]

let F be FinSequence of the carrier of G; :: thesis:
let a be Element of G; :: thesis:
assume A2: S₁[F] ; :: thesis:
A3: Product ((F ^ <*a*>) - {(1_ G)}) = Product ((F - {(1_ G)}) ^ (<*a*> - {(1_ G)})) by FINSEQ_3:73
.= (Product F) * (Product (<*a*> - {(1_ G)})) by A2, FINSOP_1:5 ;

suppose A4: a = 1_ G ; :: thesis:

then a in {(1_ G)} by TARSKI:def 1;
then <*a*> - {(1_ G)} = <*> the carrier of G by FINSEQ_3:76;
then Product (<*a*> - {(1_ G)}) = 1_ G by Th8;
hence S₁[F ^ <*a*>] by A3, A4, FINSOP_1:4; :: thesis:

end;

suppose a <> 1_ G ; :: thesis:

then not a in {(1_ G)} by TARSKI:def 1;
then <*a*> - {(1_ G)} = <*a*> by FINSEQ_3:75;
hence S₁[F ^ <*a*>] by A3, FINSOP_1:5; :: thesis:

end;

end;

end;

hence S₁[F ^ <*a*>] ; :: thesis:

end;

A5: S₁[ <*> the carrier of G] by FINSEQ_3:74;
for F being FinSequence of the carrier of G holds S₁[F] from FINSEQ_2:sch 2(A5, A1);
hence Product (F - {(1_ G)}) = Product F ; :: thesis: