let R be non empty add-cancelable add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; :: thesis:
let F be non empty Subset of R; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in F -Ideal ; :: thesis:
then consider lc being LinearCombination of F such that
A1: x = Sum lc by Th60;
lc is LeftLinearCombination of F by Th31;
hence x in F -LeftIdeal by A1, Th61; :: thesis:

end;

assume x in F -LeftIdeal ; :: thesis:
then consider lc being LeftLinearCombination of F such that
A2: x = Sum lc by Th61;
lc is LinearCombination of F by Th25;
hence x in F -Ideal by A2, Th60; :: thesis:

end;

hence F -Ideal = F -LeftIdeal by TARSKI:2; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in F -Ideal ; :: thesis:
then consider lc being LinearCombination of F such that
A3: x = Sum lc by Th60;
lc is RightLinearCombination of F by Th31;
hence x in F -RightIdeal by A3, Th62; :: thesis:

end;

assume x in F -RightIdeal ; :: thesis:
then consider lc being RightLinearCombination of F such that
A4: x = Sum lc by Th62;
lc is LinearCombination of F by Th28;
hence x in F -Ideal by A4, Th60; :: thesis:

end;

hence F -Ideal = F -RightIdeal by TARSKI:2; :: thesis: