let A1, A2 be strict MSSubAlgebra of product OAF; :: thesis: ( ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) & ( for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A2 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ) implies A1 = A2 )
assume that
A84: for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) and
A85: for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of A2 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) ; :: thesis: A1 = A2
for s being object st s in the carrier of S holds
the Sorts of A1 . s = the Sorts of A2 . s

proof

let a be object ; :: thesis: ( a in the carrier of S implies the Sorts of A1 . a = the Sorts of A2 . a )
assume a in the carrier of S ; :: thesis: the Sorts of A1 . a = the Sorts of A2 . a
then reconsider s = a as SortSymbol of S ;
thus the Sorts of A1 . a c= the Sorts of A2 . a :: according to XBOOLE_0:def 10 :: thesis: the Sorts of A2 . a c= the Sorts of A1 . a

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the Sorts of A1 . a or e in the Sorts of A2 . a )
assume A86: e in the Sorts of A1 . a ; :: thesis: e in the Sorts of A2 . a
the Sorts of A1 is MSSubset of (product OAF) by MSUALG_2:def 9;
then the Sorts of A1 c= the Sorts of (product OAF) by PBOOLE:def 18;
then the Sorts of A1 c= SORTS OAF by PRALG_2:12;
then the Sorts of A1 . s c= (SORTS OAF) . s by PBOOLE:def 2;
then reconsider f = e as Element of (SORTS OAF) . s by A86;
for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j by A84, A86;
hence e in the Sorts of A2 . a by A85; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the Sorts of A2 . a or e in the Sorts of A1 . a )
assume A87: e in the Sorts of A2 . a ; :: thesis: e in the Sorts of A1 . a
the Sorts of A2 is MSSubset of (product OAF) by MSUALG_2:def 9;
then the Sorts of A2 c= the Sorts of (product OAF) by PBOOLE:def 18;
then the Sorts of A2 c= SORTS OAF by PRALG_2:12;
then the Sorts of A2 . s c= (SORTS OAF) . s by PBOOLE:def 2;
then reconsider f = e as Element of (SORTS OAF) . s by A87;
for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j by A85, A87;
hence e in the Sorts of A1 . a by A84; :: thesis: verum

end;

hence A1 = A2 by MSUALG_2:9, PBOOLE:3; :: thesis: verum