let G be Group; :: thesis: for F being FinSequence of the carrier of G holds Product (F - {(1_ G)}) = Product F
let F be FinSequence of the carrier of G; :: thesis: Product (F - {(1_ G)}) = Product F
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*>]

proof

let F be FinSequence of the carrier of G; :: thesis: for a being Element of G st S₁[F] holds
S₁[F ^ <*a*>]
let a be Element of G; :: thesis: ( S₁[F] implies S₁[F ^ <*a*>] )
assume A2: S₁[F] ; :: thesis: S₁[F ^ <*a*>]
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 ;

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

per cases ( a = 1_ G or a <> 1_ G ) ;

suppose A4: a = 1_ G ; :: thesis: S₁[F ^ <*a*>]

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: verum

end;

suppose a <> 1_ G ; :: thesis: S₁[F ^ <*a*>]

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: verum

end;

end;

end;

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

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: verum