let T be non empty RelStr ; :: thesis: for A, B being Subset of T
for n being Nat holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
let A, B be Subset of T; :: thesis: for n being Nat holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
let n be Nat; :: thesis: Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
for n being Nat holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n)

proof

defpred S₁[ Nat] means (Fcl (A \/ B)) . $1 = ((Fcl A) . $1) \/ ((Fcl B) . $1);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
(Fcl (A \/ B)) . (k + 1) = (Fcl ((A \/ B),k)) ^b by Def2
.= ((Fcl (A,k)) ^b) \/ ((Fcl (B,k)) ^b) by A2, Th8
.= (Fcl (A,(k + 1))) \/ ((Fcl (B,k)) ^b) by Def2
.= ((Fcl A) . (k + 1)) \/ ((Fcl B) . (k + 1)) by Def2 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(Fcl (A \/ B)) . 0 = A \/ B by Def2
.= ((Fcl A) . 0) \/ B by Def2
.= ((Fcl A) . 0) \/ ((Fcl B) . 0) by Def2 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence for n being Nat holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n) ; :: thesis: verum

end;

hence Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) ; :: thesis: verum