for PC1, PC2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) holds
PC1 = PC2

proof

let PC1, PC2 be MSAlgebra-Family of I,S; :: thesis: ( ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) implies PC1 = PC2 )
assume A5: ( ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) ) ; :: thesis: PC1 = PC2

now

let i1 be set ; :: thesis: ( i1 in I implies PC1 . i1 = PC2 . i1 )
assume i1 in I ; :: thesis: PC1 . i1 = PC2 . i1
then reconsider i9 = i1 as Element of I ;
( ex Ji1 being non empty set ex Cs1 being MSAlgebra-Family of Ji1,S st
( Ji1 = J . i9 & Cs1 = C . i9 & PC1 . i9 = product Cs1 ) & ex Ji2 being non empty set ex Cs2 being MSAlgebra-Family of Ji2,S st
( Ji2 = J . i9 & Cs2 = C . i9 & PC2 . i9 = product Cs2 ) ) by A5;
hence PC1 . i1 = PC2 . i1 ; :: thesis: verum

end;

hence PC1 = PC2 by PBOOLE:3; :: thesis: verum

end;

hence for b₁, b₂ being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b₁ . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b₂ . i = product Cs ) ) holds
b₁ = b₂ ; :: thesis: verum