let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for I being non empty Subset of REAL st I = {1,2,3} & Sigma = bool {1,2,3,4} & Omega = {1,2,3,4} holds
ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 & MyFunc is Filtration of I,Sigma )
let Sigma be SigmaField of Omega; :: thesis: for I being non empty Subset of REAL st I = {1,2,3} & Sigma = bool {1,2,3,4} & Omega = {1,2,3,4} holds
ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 & MyFunc is Filtration of I,Sigma )
let I be non empty Subset of REAL; :: thesis: ( I = {1,2,3} & Sigma = bool {1,2,3,4} & Omega = {1,2,3,4} implies ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 & MyFunc is Filtration of I,Sigma ) )
assume A0: ( I = {1,2,3} & Sigma = bool {1,2,3,4} & Omega = {1,2,3,4} ) ; :: thesis: ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 & MyFunc is Filtration of I,Sigma )
consider MyFunc being ManySortedSigmaField of I,Sigma such that
A1: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 ) by A0, Th3;
A3: for s, t being Element of I st s <= t holds
MyFunc . s is Subset of (MyFunc . t)

proof

let s, t be Element of I; :: thesis: ( s <= t implies MyFunc . s is Subset of (MyFunc . t) )
assume B10: s <= t ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

per cases ( ( s = 1 & ( t = 1 or t = 3 ) ) or ( s = 1 & t = 2 ) or ( s = 2 & ( t = 1 or t = 2 or t = 3 ) ) or ( s = 3 & ( t = 1 or t = 2 or t = 3 ) ) ) by A0, ENUMSET1:def 1;

suppose ( s = 1 & ( t = 1 or t = 3 ) ) ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

hence MyFunc . s is Subset of (MyFunc . t) by A1; :: thesis: verum

end;

suppose ( s = 1 & t = 2 ) ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

hence MyFunc . s is Subset of (MyFunc . t) by A1, XX1; :: thesis: verum

end;

suppose ( s = 2 & ( t = 1 or t = 2 or t = 3 ) ) ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

hence MyFunc . s is Subset of (MyFunc . t) by A1, B10; :: thesis: verum

end;

suppose ( s = 3 & ( t = 1 or t = 2 or t = 3 ) ) ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

hence MyFunc . s is Subset of (MyFunc . t) by B10, A1; :: thesis: verum

end;

end;

end;

for t being Element of I holds MyFunc . t c= Sigma by A0;
then MyFunc is Filtration of I,Sigma by A3, Def2000;
hence ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 & MyFunc is Filtration of I,Sigma ) by A1; :: thesis: verum