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

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

hence
A1 = A2
by MSUALG_2:9, PBOOLE:3; :: thesis: verum
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

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;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 A2 . a or e in the Sorts of A1 . a )
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;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

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