let X be set ; :: thesis: for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)
let F1 be FinSequence of bool X; :: thesis: Intersection F1 = meet (rng F1)
per cases ( F1 <> {} or F1 = {} ) ;
suppose A1: F1 <> {} ; :: thesis: Intersection F1 = meet (rng F1)
now :: thesis: for x being object holds
( x in Intersection F1 iff x in meet (rng F1) )
let x be object ; :: thesis: ( x in Intersection F1 iff x in meet (rng F1) )
( x in Intersection F1 iff for n being Nat st n in dom F1 holds
x in F1 . n ) by A1, Th51;
hence ( x in Intersection F1 iff x in meet (rng F1) ) by A1, Th52; :: thesis: verum
end;
hence Intersection F1 = meet (rng F1) by TARSKI:2; :: thesis: verum
end;
suppose F1 = {} ; :: thesis: Intersection F1 = meet (rng F1)
hence Intersection F1 = meet (rng F1) by Def6, RELAT_1:38, SETFAM_1:1; :: thesis: verum
end;
end;