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 B1: s <= t ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

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

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

MyFunc . s is Subset of (MyFunc . t)

proof

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

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

then ( MyFunc . t = MyFunc . 1 & MyFunc . s = MyFunc . 1 ) by SUPP1;
hence MyFunc . s is Subset of (MyFunc . t) ; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

MyFunc . s is Subset of (MyFunc . t)

proof

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

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

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

end;

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

then ( MyFunc . t = MyFunc . 2 & MyFunc . s = MyFunc . 2 ) by SUPP1;
hence MyFunc . s is Subset of (MyFunc . t) ; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

suppose SUPP1: s = 3 ; :: thesis: MyFunc . s is Subset of (MyFunc . t)

MyFunc . s is Subset of (MyFunc . t)

proof

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

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

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

end;

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

then ( MyFunc . t = MyFunc . 3 & MyFunc . s = MyFunc . 3 ) by SUPP1;
hence MyFunc . s is Subset of (MyFunc . t) ; :: thesis: verum

end;

end;

end;

hence MyFunc . s is Subset of (MyFunc . t) ; :: 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